--  Copyright (C) 2011-2 Ganesh Sittampalam
--
--  BSD3

module Darcs.Patch.Rebase.Name
    ( RebaseName(..)
    , commuteNamePrim, commutePrimName
    , commuterIdNamed, commuterNamedId
    , commuteNameNamed, commuteNamedName
    , pushFixupName
    ) where

import Darcs.Prelude

import Darcs.Patch.Commute ( Commute(..) )
import Darcs.Patch.CommuteFn ( CommuteFn, commuterIdFL, commuterFLId )
import Darcs.Patch.Info ( PatchInfo, showPatchInfo, readPatchInfo )
import Darcs.Patch.Inspect ( PatchInspect(..) )
import Darcs.Patch.Invert ( Invert(..) )
import Darcs.Patch.Named ( Named(..) )
import Darcs.Patch.Read ( ReadPatch(..) )
import Darcs.Patch.Show ( ShowPatchBasic(..), ShowPatch(..) )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) )
import Darcs.Patch.Witnesses.Maybe ( Maybe2(..) )
import Darcs.Patch.Witnesses.Ordered ( (:>)(..), FL(..) )
import Darcs.Patch.Witnesses.Sealed ( Sealed(..) )
import Darcs.Patch.Witnesses.Show ( Show1, Show2 )
import Darcs.Patch.Witnesses.Unsafe ( unsafeCoerceP, unsafeCoercePEnd )

import Darcs.Patch.Rebase.PushFixup ( PushFixupFn )

import Darcs.Util.Parser ( lexString )
import Darcs.Util.Printer ( empty, blueText, ($$) )

import Control.Applicative ( (<|>) )
import qualified Data.ByteString.Char8 as BC ( pack )

-- Note: in principle this is a general concept not limited to
-- rebase, and we might be able to generalise this type and
-- refactor named patches to use it too.

-- | A 'RebaseName' encapsulates the concept of the name of a patch,
-- without any contents. This allows us to track explicit dependencies
-- in the rebase state, changing them to follow uses of amend-record
-- or unsuspend on a depended-on patch, and warning the user if any
-- are lost entirely.
data RebaseName wX wY where
  AddName :: PatchInfo -> RebaseName wX wY
  DelName :: PatchInfo -> RebaseName wX wY
  Rename :: PatchInfo -> PatchInfo -> RebaseName wX wY
    deriving (RebaseName wX wY -> RebaseName wX wY -> Bool
(RebaseName wX wY -> RebaseName wX wY -> Bool)
-> (RebaseName wX wY -> RebaseName wX wY -> Bool)
-> Eq (RebaseName wX wY)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall wX wY. RebaseName wX wY -> RebaseName wX wY -> Bool
$c== :: forall wX wY. RebaseName wX wY -> RebaseName wX wY -> Bool
== :: RebaseName wX wY -> RebaseName wX wY -> Bool
$c/= :: forall wX wY. RebaseName wX wY -> RebaseName wX wY -> Bool
/= :: RebaseName wX wY -> RebaseName wX wY -> Bool
Eq, Int -> RebaseName wX wY -> ShowS
[RebaseName wX wY] -> ShowS
RebaseName wX wY -> String
(Int -> RebaseName wX wY -> ShowS)
-> (RebaseName wX wY -> String)
-> ([RebaseName wX wY] -> ShowS)
-> Show (RebaseName wX wY)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall wX wY. Int -> RebaseName wX wY -> ShowS
forall wX wY. [RebaseName wX wY] -> ShowS
forall wX wY. RebaseName wX wY -> String
$cshowsPrec :: forall wX wY. Int -> RebaseName wX wY -> ShowS
showsPrec :: Int -> RebaseName wX wY -> ShowS
$cshow :: forall wX wY. RebaseName wX wY -> String
show :: RebaseName wX wY -> String
$cshowList :: forall wX wY. [RebaseName wX wY] -> ShowS
showList :: [RebaseName wX wY] -> ShowS
Show)

instance Show1 (RebaseName wX)

instance Show2 RebaseName

instance ShowPatchBasic RebaseName where
   showPatch :: forall wX wY. ShowPatchFor -> RebaseName wX wY -> Doc
showPatch ShowPatchFor
f (AddName PatchInfo
n) = String -> Doc
blueText String
"addname" Doc -> Doc -> Doc
$$ ShowPatchFor -> PatchInfo -> Doc
showPatchInfo ShowPatchFor
f PatchInfo
n
   showPatch ShowPatchFor
f (DelName PatchInfo
n) = String -> Doc
blueText String
"delname" Doc -> Doc -> Doc
$$ ShowPatchFor -> PatchInfo -> Doc
showPatchInfo ShowPatchFor
f PatchInfo
n
   showPatch ShowPatchFor
f (Rename PatchInfo
old PatchInfo
new) = String -> Doc
blueText String
"rename" Doc -> Doc -> Doc
$$ ShowPatchFor -> PatchInfo -> Doc
showPatchInfo ShowPatchFor
f PatchInfo
old Doc -> Doc -> Doc
$$ ShowPatchFor -> PatchInfo -> Doc
showPatchInfo ShowPatchFor
f PatchInfo
new

instance ShowPatch RebaseName where
   summary :: forall wX wY. RebaseName wX wY -> Doc
summary RebaseName wX wY
_ = Doc
empty -- TODO improve this?
   summaryFL :: forall wX wY. FL RebaseName wX wY -> Doc
summaryFL FL RebaseName wX wY
_ = Doc
empty

instance ReadPatch RebaseName where
   readPatch' :: forall wX. Parser (Sealed (RebaseName wX))
readPatch' = Parser ByteString (Sealed (RebaseName wX))
forall wX. Parser (Sealed (RebaseName wX))
readAddName Parser ByteString (Sealed (RebaseName wX))
-> Parser ByteString (Sealed (RebaseName wX))
-> Parser ByteString (Sealed (RebaseName wX))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ByteString (Sealed (RebaseName wX))
forall wX. Parser (Sealed (RebaseName wX))
readDelName Parser ByteString (Sealed (RebaseName wX))
-> Parser ByteString (Sealed (RebaseName wX))
-> Parser ByteString (Sealed (RebaseName wX))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ByteString (Sealed (RebaseName wX))
forall wX. Parser (Sealed (RebaseName wX))
readRename
     where
       readAddName :: Parser ByteString (Sealed (RebaseName wX))
readAddName = do ByteString -> Parser ()
lexString (String -> ByteString
BC.pack String
"addname")
                        PatchInfo
n <- Parser PatchInfo
readPatchInfo
                        Sealed (RebaseName wX)
-> Parser ByteString (Sealed (RebaseName wX))
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (RebaseName wX Any -> Sealed (RebaseName wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
n))
       readDelName :: Parser ByteString (Sealed (RebaseName wX))
readDelName = do ByteString -> Parser ()
lexString (String -> ByteString
BC.pack String
"delname")
                        PatchInfo
n <- Parser PatchInfo
readPatchInfo
                        Sealed (RebaseName wX)
-> Parser ByteString (Sealed (RebaseName wX))
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (RebaseName wX Any -> Sealed (RebaseName wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
n))
       readRename :: Parser ByteString (Sealed (RebaseName wX))
readRename  = do ByteString -> Parser ()
lexString (String -> ByteString
BC.pack String
"rename")
                        PatchInfo
old <- Parser PatchInfo
readPatchInfo
                        PatchInfo
new <- Parser PatchInfo
readPatchInfo
                        Sealed (RebaseName wX)
-> Parser ByteString (Sealed (RebaseName wX))
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (RebaseName wX Any -> Sealed (RebaseName wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (PatchInfo -> PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old PatchInfo
new))

instance Commute RebaseName where
   commute :: forall wX wY.
(:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
commute (AddName PatchInfo
n1 :> AddName PatchInfo
n2)
      | PatchInfo
n1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
n2 = String -> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
      | Bool
otherwise = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
n2 RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
n1)
   commute (DelName PatchInfo
n1 :> DelName PatchInfo
n2)
      | PatchInfo
n1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
n2 = String -> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
      | Bool
otherwise = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
n2 RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
n1)
   commute (AddName PatchInfo
n1 :> DelName PatchInfo
n2)
      | PatchInfo
n1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= PatchInfo
n2 = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
n2 RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
n1)
      | Bool
otherwise = Maybe ((:>) RebaseName RebaseName wX wY)
forall a. Maybe a
Nothing
   commute (DelName PatchInfo
n1 :> AddName PatchInfo
n2)
      | PatchInfo
n1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= PatchInfo
n2 = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
n2 RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
n1)
      | Bool
otherwise = Maybe ((:>) RebaseName RebaseName wX wY)
forall a. Maybe a
Nothing
   commute (Rename PatchInfo
old PatchInfo
new :> AddName PatchInfo
n)
      | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
old = Maybe ((:>) RebaseName RebaseName wX wY)
forall a. Maybe a
Nothing
      | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
new = String -> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case" -- precondition of Add is that n doesn't exist
      | Bool
otherwise = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
n RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old PatchInfo
new)
   commute (AddName PatchInfo
n :> Rename PatchInfo
old PatchInfo
new)
      | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
old = Maybe ((:>) RebaseName RebaseName wX wY)
forall a. Maybe a
Nothing
      | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
new = String -> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case" -- precondition of Rename is that new doesn't exist
      | Bool
otherwise = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old PatchInfo
new RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
n)
   commute (Rename PatchInfo
old PatchInfo
new :> DelName PatchInfo
n)
      | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
old = String -> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case" -- precondition of Del is that n does exist
      | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
new = Maybe ((:>) RebaseName RebaseName wX wY)
forall a. Maybe a
Nothing
      | Bool
otherwise = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
n RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old PatchInfo
new)
   commute (DelName PatchInfo
n :> Rename PatchInfo
old PatchInfo
new)
      | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
old = String -> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case" -- precondition of Rename is that old does exist
      | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
new = Maybe ((:>) RebaseName RebaseName wX wY)
forall a. Maybe a
Nothing
      | Bool
otherwise = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old PatchInfo
new RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
n)
   commute (Rename PatchInfo
old1 PatchInfo
new1 :> Rename PatchInfo
old2 PatchInfo
new2)
      | PatchInfo
old1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
old2 = String -> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
      | PatchInfo
new1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
new2 = String -> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
      | PatchInfo
old1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
new2 = Maybe ((:>) RebaseName RebaseName wX wY)
forall a. Maybe a
Nothing
      | PatchInfo
new1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
old2 = Maybe ((:>) RebaseName RebaseName wX wY)
forall a. Maybe a
Nothing
      | Bool
otherwise = (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old2 PatchInfo
new2 RebaseName wX Any
-> RebaseName Any wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old1 PatchInfo
new1)

instance Invert RebaseName where
   invert :: forall wX wY. RebaseName wX wY -> RebaseName wY wX
invert (AddName PatchInfo
n) = PatchInfo -> RebaseName wY wX
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
n
   invert (DelName PatchInfo
n) = PatchInfo -> RebaseName wY wX
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
n
   invert (Rename PatchInfo
old PatchInfo
new) = PatchInfo -> PatchInfo -> RebaseName wY wX
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
new PatchInfo
old

instance PatchInspect RebaseName where
    listTouchedFiles :: forall wX wY. RebaseName wX wY -> [AnchoredPath]
listTouchedFiles RebaseName wX wY
_ = []
    hunkMatches :: forall wX wY. (ByteString -> Bool) -> RebaseName wX wY -> Bool
hunkMatches ByteString -> Bool
_ RebaseName wX wY
_ = Bool
False

instance Eq2 RebaseName where
   RebaseName wA wB
p1 =\/= :: forall wA wB wC.
RebaseName wA wB -> RebaseName wA wC -> EqCheck wB wC
=\/= RebaseName wA wC
p2
      | RebaseName wA wB
p1 RebaseName wA wB -> RebaseName wA wB -> Bool
forall a. Eq a => a -> a -> Bool
== RebaseName wA wC -> RebaseName wA wB
forall (a :: * -> * -> *) wX wY1 wY2. a wX wY1 -> a wX wY2
unsafeCoercePEnd RebaseName wA wC
p2 = EqCheck wB wB -> EqCheck wB wC
forall (a :: * -> * -> *) wX wY1 wY2. a wX wY1 -> a wX wY2
unsafeCoercePEnd EqCheck wB wB
forall wA. EqCheck wA wA
IsEq
      | Bool
otherwise = EqCheck wB wC
forall wA wB. EqCheck wA wB
NotEq

-- |Commute a 'RebaseName' and a primitive patch. They trivially
-- commute so this just involves changing the witnesses.
-- This is unsafe if the patch being commuted actually has a
-- name (e.g. Named or PatchInfo - PrimWithName is ok),
commuteNamePrim :: (RebaseName :> prim) wX wY -> (prim :> RebaseName) wX wY
commuteNamePrim :: forall (prim :: * -> * -> *) wX wY.
(:>) RebaseName prim wX wY -> (:>) prim RebaseName wX wY
commuteNamePrim (RebaseName wX wZ
n :> prim wZ wY
f) = prim wZ wY -> prim wX Any
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP prim wZ wY
f prim wX Any -> RebaseName Any wY -> (:>) prim RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wX wZ -> RebaseName Any wY
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP RebaseName wX wZ
n

-- |Commute a primitive patch and a 'RebaseName'. They trivially
-- commute so this just involves changing the witnesses.
-- This is unsafe if the patch being commuted actually has a
-- name (e.g. Named or PatchInfo - PrimWithName is ok),
commutePrimName :: (prim :> RebaseName) wX wY -> (RebaseName :> prim) wX wY
commutePrimName :: forall (prim :: * -> * -> *) wX wY.
(:>) prim RebaseName wX wY -> (:>) RebaseName prim wX wY
commutePrimName (prim wX wZ
f :> RebaseName wZ wY
n) = RebaseName wZ wY -> RebaseName wX Any
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP RebaseName wZ wY
n RebaseName wX Any -> prim Any wY -> (:>) RebaseName prim wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wX wZ -> prim Any wY
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP prim wX wZ
f

-- commuterIdNamed and commuterNamedId are defined here rather than in
-- Named given that they are unsafe, to reduce the chances of them
-- being used inappropriately.

-- |Commute an unnamed patch with a named patch. This is unsafe if the
-- second patch actually does have a name (e.g. Named, PatchInfoAnd, etc),
-- as it won't check the explicit dependencies.
commuterIdNamed :: CommuteFn p1 p2 -> CommuteFn p1 (Named p2)
commuterIdNamed :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (Named p2)
commuterIdNamed CommuteFn p1 p2
commuter (p1 wX wZ
p1 :> NamedP PatchInfo
n2 [PatchInfo]
d2 FL p2 wZ wY
p2) =
   do FL p2 wX wZ
p2' :> p1 wZ wY
p1' <- CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL (:>) p1 p2 wX wY -> Maybe ((:>) p2 p1 wX wY)
CommuteFn p1 p2
commuter (p1 wX wZ
p1 p1 wX wZ -> FL p2 wZ wY -> (:>) p1 (FL p2) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wZ wY
p2)
      (:>) (Named p2) p1 wX wY -> Maybe ((:>) (Named p2) p1 wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (PatchInfo -> [PatchInfo] -> FL p2 wX wZ -> Named p2 wX wZ
forall (p :: * -> * -> *) wX wY.
PatchInfo -> [PatchInfo] -> FL p wX wY -> Named p wX wY
NamedP PatchInfo
n2 [PatchInfo]
d2 FL p2 wX wZ
p2' Named p2 wX wZ -> p1 wZ wY -> (:>) (Named p2) p1 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wZ wY
p1')

-- |Commute an unnamed patch with a named patch. This is unsafe if the
-- first patch actually does have a name (e.g. Named, PatchInfoAnd, etc),
-- as it won't check the explicit dependencies.
commuterNamedId :: CommuteFn p1 p2 -> CommuteFn (Named p1) p2
commuterNamedId :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (Named p1) p2
commuterNamedId CommuteFn p1 p2
commuter (NamedP PatchInfo
n1 [PatchInfo]
d1 FL p1 wX wZ
p1 :> p2 wZ wY
p2) =
   do p2 wX wZ
p2' :> FL p1 wZ wY
p1' <- CommuteFn p1 p2 -> CommuteFn (FL p1) p2
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId (:>) p1 p2 wX wY -> Maybe ((:>) p2 p1 wX wY)
CommuteFn p1 p2
commuter (FL p1 wX wZ
p1 FL p1 wX wZ -> p2 wZ wY -> (:>) (FL p1) p2 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
p2)
      (:>) p2 (Named p1) wX wY -> Maybe ((:>) p2 (Named p1) wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
p2' p2 wX wZ -> Named p1 wZ wY -> (:>) p2 (Named p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> [PatchInfo] -> FL p1 wZ wY -> Named p1 wZ wY
forall (p :: * -> * -> *) wX wY.
PatchInfo -> [PatchInfo] -> FL p wX wY -> Named p wX wY
NamedP PatchInfo
n1 [PatchInfo]
d1 FL p1 wZ wY
p1')

-- |Commute a name patch and a named patch. In most cases this is
-- trivial but we do need to check explicit dependencies.
commuteNameNamed :: CommuteFn RebaseName (Named p)
commuteNameNamed :: forall (p :: * -> * -> *) wX wY.
(:>) RebaseName (Named p) wX wY
-> Maybe ((:>) (Named p) RebaseName wX wY)
commuteNameNamed (AddName PatchInfo
an :> p :: Named p wZ wY
p@(NamedP PatchInfo
pn [PatchInfo]
deps FL p wZ wY
_))
  | PatchInfo
an PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
pn = String -> Maybe ((:>) (Named p) RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
  | PatchInfo
an PatchInfo -> [PatchInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PatchInfo]
deps = Maybe ((:>) (Named p) RebaseName wX wY)
forall a. Maybe a
Nothing
  | Bool
otherwise = (:>) (Named p) RebaseName wX wY
-> Maybe ((:>) (Named p) RebaseName wX wY)
forall a. a -> Maybe a
Just (Named p wZ wY -> Named p wX Any
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP Named p wZ wY
p Named p wX Any
-> RebaseName Any wY -> (:>) (Named p) RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
an)
commuteNameNamed (DelName PatchInfo
dn :> p :: Named p wZ wY
p@(NamedP PatchInfo
pn [PatchInfo]
deps FL p wZ wY
_))
  -- this case can arise if a patch is suspended then a fresh copy is pulled from another repo
  | PatchInfo
dn PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
pn = Maybe ((:>) (Named p) RebaseName wX wY)
forall a. Maybe a
Nothing
  | PatchInfo
dn PatchInfo -> [PatchInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PatchInfo]
deps = String -> Maybe ((:>) (Named p) RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
  | Bool
otherwise = (:>) (Named p) RebaseName wX wY
-> Maybe ((:>) (Named p) RebaseName wX wY)
forall a. a -> Maybe a
Just (Named p wZ wY -> Named p wX Any
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP Named p wZ wY
p Named p wX Any
-> RebaseName Any wY -> (:>) (Named p) RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
dn)
commuteNameNamed (Rename PatchInfo
old PatchInfo
new :> NamedP PatchInfo
pn [PatchInfo]
deps FL p wZ wY
body)
  | PatchInfo
old PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
pn = String -> Maybe ((:>) (Named p) RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
  | PatchInfo
new PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
pn = String -> Maybe ((:>) (Named p) RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
  | PatchInfo
old PatchInfo -> [PatchInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PatchInfo]
deps = String -> Maybe ((:>) (Named p) RebaseName wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
  | Bool
otherwise =
      let newdeps :: [PatchInfo]
newdeps = (PatchInfo -> PatchInfo) -> [PatchInfo] -> [PatchInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\PatchInfo
dep -> if PatchInfo
new PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
dep then PatchInfo
old else PatchInfo
dep) [PatchInfo]
deps
      in (:>) (Named p) RebaseName wX wY
-> Maybe ((:>) (Named p) RebaseName wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> [PatchInfo] -> FL p wX Any -> Named p wX Any
forall (p :: * -> * -> *) wX wY.
PatchInfo -> [PatchInfo] -> FL p wX wY -> Named p wX wY
NamedP PatchInfo
pn [PatchInfo]
newdeps (FL p wZ wY -> FL p wX Any
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP FL p wZ wY
body) Named p wX Any
-> RebaseName Any wY -> (:>) (Named p) RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> PatchInfo -> RebaseName Any wY
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old PatchInfo
new)

-- |Commute a named patch and a name patch. In most cases this is
-- trivial but we do need to check explicit dependencies.
commuteNamedName :: CommuteFn (Named p) RebaseName
commuteNamedName :: forall (p :: * -> * -> *) wX wY.
(:>) (Named p) RebaseName wX wY
-> Maybe ((:>) RebaseName (Named p) wX wY)
commuteNamedName (p :: Named p wX wZ
p@(NamedP PatchInfo
pn [PatchInfo]
deps FL p wX wZ
_) :> AddName PatchInfo
an)
  | PatchInfo
an PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
pn = String -> Maybe ((:>) RebaseName (Named p) wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"  -- the NamedP introduces pn, then AddName introduces it again
  | PatchInfo
an PatchInfo -> [PatchInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PatchInfo]
deps = String -> Maybe ((:>) RebaseName (Named p) wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case" -- the NamedP depends on an before it is introduced
  | Bool
otherwise = (:>) RebaseName (Named p) wX wY
-> Maybe ((:>) RebaseName (Named p) wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
an RebaseName wX Any
-> Named p Any wY -> (:>) RebaseName (Named p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Named p wX wZ -> Named p Any wY
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP Named p wX wZ
p)
commuteNamedName (p :: Named p wX wZ
p@(NamedP PatchInfo
pn [PatchInfo]
deps FL p wX wZ
_) :> DelName PatchInfo
dn)
  | PatchInfo
dn PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
pn = Maybe ((:>) RebaseName (Named p) wX wY)
forall a. Maybe a
Nothing
  | PatchInfo
dn PatchInfo -> [PatchInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PatchInfo]
deps = Maybe ((:>) RebaseName (Named p) wX wY)
forall a. Maybe a
Nothing
  | Bool
otherwise = (:>) RebaseName (Named p) wX wY
-> Maybe ((:>) RebaseName (Named p) wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
dn RebaseName wX Any
-> Named p Any wY -> (:>) RebaseName (Named p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Named p wX wZ -> Named p Any wY
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP Named p wX wZ
p)
commuteNamedName (NamedP PatchInfo
pn [PatchInfo]
deps FL p wX wZ
body :> Rename PatchInfo
old PatchInfo
new)
  | PatchInfo
old PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
pn = Maybe ((:>) RebaseName (Named p) wX wY)
forall a. Maybe a
Nothing
  | PatchInfo
new PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
pn = String -> Maybe ((:>) RebaseName (Named p) wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
  | PatchInfo
new PatchInfo -> [PatchInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PatchInfo]
deps = String -> Maybe ((:>) RebaseName (Named p) wX wY)
forall a. HasCallStack => String -> a
error String
"impossible case"
  | Bool
otherwise =
      let newdeps :: [PatchInfo]
newdeps = (PatchInfo -> PatchInfo) -> [PatchInfo] -> [PatchInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\PatchInfo
dep -> if PatchInfo
old PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
dep then PatchInfo
new else PatchInfo
dep) [PatchInfo]
deps
      in (:>) RebaseName (Named p) wX wY
-> Maybe ((:>) RebaseName (Named p) wX wY)
forall a. a -> Maybe a
Just (PatchInfo -> PatchInfo -> RebaseName wX Any
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old PatchInfo
new RebaseName wX Any
-> Named p Any wY -> (:>) RebaseName (Named p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchInfo -> [PatchInfo] -> FL p Any wY -> Named p Any wY
forall (p :: * -> * -> *) wX wY.
PatchInfo -> [PatchInfo] -> FL p wX wY -> Named p wX wY
NamedP PatchInfo
pn [PatchInfo]
newdeps (FL p wX wZ -> FL p Any wY
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP FL p wX wZ
body))

canonizeNamePair :: (RebaseName :> RebaseName) wX wY -> FL RebaseName wX wY
canonizeNamePair :: forall wX wY.
(:>) RebaseName RebaseName wX wY -> FL RebaseName wX wY
canonizeNamePair (AddName PatchInfo
n :> Rename PatchInfo
old PatchInfo
new) | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
old = PatchInfo -> RebaseName wX wY
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
new RebaseName wX wY -> FL RebaseName wY wY -> FL RebaseName wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL RebaseName wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
canonizeNamePair (Rename PatchInfo
old PatchInfo
new :> DelName PatchInfo
n) | PatchInfo
n PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
new = PatchInfo -> RebaseName wX wY
forall wX wY. PatchInfo -> RebaseName wX wY
DelName PatchInfo
old RebaseName wX wY -> FL RebaseName wY wY -> FL RebaseName wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL RebaseName wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
canonizeNamePair (Rename PatchInfo
old1 PatchInfo
new1 :> Rename PatchInfo
old2 PatchInfo
new2) | PatchInfo
new1 PatchInfo -> PatchInfo -> Bool
forall a. Eq a => a -> a -> Bool
== PatchInfo
old2 = PatchInfo -> PatchInfo -> RebaseName wX wY
forall wX wY. PatchInfo -> PatchInfo -> RebaseName wX wY
Rename PatchInfo
old1 PatchInfo
new2 RebaseName wX wY -> FL RebaseName wY wY -> FL RebaseName wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL RebaseName wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
canonizeNamePair (RebaseName wX wZ
n1 :> RebaseName wZ wY
n2) = RebaseName wX wZ
n1 RebaseName wX wZ -> FL RebaseName wZ wY -> FL RebaseName wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: RebaseName wZ wY
n2 RebaseName wZ wY -> FL RebaseName wY wY -> FL RebaseName wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL RebaseName wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL

pushFixupName :: PushFixupFn RebaseName RebaseName (FL RebaseName) (Maybe2 RebaseName)
pushFixupName :: PushFixupFn
  RebaseName RebaseName (FL RebaseName) (Maybe2 RebaseName)
pushFixupName (RebaseName wX wZ
n1 :> RebaseName wZ wY
n2)
 | EqCheck wX wY
IsEq <- EqCheck wX wY
isInverse = FL RebaseName wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL RebaseName wX wX
-> Maybe2 RebaseName wX wY
-> (:>) (FL RebaseName) (Maybe2 RebaseName) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 RebaseName wX wX
Maybe2 RebaseName wX wY
forall (p :: * -> * -> *) wX. Maybe2 p wX wX
Nothing2
 | Bool
otherwise
   = case (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall wX wY.
(:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (RebaseName wX wZ
n1 RebaseName wX wZ
-> RebaseName wZ wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY
n2) of
       Maybe ((:>) RebaseName RebaseName wX wY)
Nothing -> ((:>) RebaseName RebaseName wX wY -> FL RebaseName wX wY
forall wX wY.
(:>) RebaseName RebaseName wX wY -> FL RebaseName wX wY
canonizeNamePair (RebaseName wX wZ
n1 RebaseName wX wZ
-> RebaseName wZ wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY
n2)) FL RebaseName wX wY
-> Maybe2 RebaseName wY wY
-> (:>) (FL RebaseName) (Maybe2 RebaseName) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 RebaseName wY wY
forall (p :: * -> * -> *) wX. Maybe2 p wX wX
Nothing2
       Just (RebaseName wX wZ
n2' :> RebaseName wZ wY
n1') -> (RebaseName wX wZ
n2' RebaseName wX wZ -> FL RebaseName wZ wZ -> FL RebaseName wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL RebaseName wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL RebaseName wX wZ
-> Maybe2 RebaseName wZ wY
-> (:>) (FL RebaseName) (Maybe2 RebaseName) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY -> Maybe2 RebaseName wZ wY
forall (p :: * -> * -> *) wX wY. p wX wY -> Maybe2 p wX wY
Just2 RebaseName wZ wY
n1'
  where isInverse :: EqCheck wX wY
isInverse = RebaseName wX wZ -> RebaseName wZ wX
forall wX wY. RebaseName wX wY -> RebaseName wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert RebaseName wX wZ
n1 RebaseName wZ wX -> RebaseName wZ wY -> EqCheck wX wY
forall wA wB wC.
RebaseName wA wB -> RebaseName wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= RebaseName wZ wY
n2