--- | This breaks a 'Coercion' with 'CoercionKind' @T A B C :=: T D E F@ into
--- a list of 'Coercion's of kinds @A :=: D@, @B :=: E@ and @E :=: F@. Hence:
+-- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into
+-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
--
-- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
decomposeCo :: Arity -> Coercion -> [Coercion]
--
-- > decomposeCo 3 c = [right (left (left c)), right (left c), right c]
decomposeCo :: Arity -> Coercion -> [Coercion]
--
-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
-- See also 'coercionKindPredTy'
--
-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
-- See also 'coercionKindPredTy'
mkSymCoercion :: Coercion -> Coercion
-- ^ Create a symmetric version of the given 'Coercion' that asserts equality between
mkSymCoercion :: Coercion -> Coercion
-- ^ Create a symmetric version of the given 'Coercion' that asserts equality between
--
-- This function attempts to simplify the generated 'Coercion' by removing redundant applications
-- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that
--
-- This function attempts to simplify the generated 'Coercion' by removing redundant applications
-- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that
(TyConApp tycon args, substTyWith tvs args rhs_ty)
-- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
(TyConApp tycon args, substTyWith tvs args rhs_ty)
-- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type
-- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
-- representation tycon.
mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon
-- the coercion tycon built here, @F@ the family tycon and @R@ the (derived)
-- representation tycon.
mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon
coArity = length tvs
rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs],
TyConApp family instTys, -- sigma (F ts)
coArity = length tvs
rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs],
TyConApp family instTys, -- sigma (F ts)
-- Helper for left and right. Finds coercion kind of its input and
-- returns the left and right projections of the coercion...
--
-- Helper for left and right. Finds coercion kind of its input and
-- returns the left and right projections of the coercion...
--
--- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
+-- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2))
splitCoercionKindOf co
| Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
, Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1
splitCoercionKindOf co
| Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
, Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1