mkCoercion,
mkSymCoercion, mkTransCoercion,
mkLeftCoercion, mkRightCoercion, mkRightCoercions,
- mkInstCoercion, mkAppCoercion,
- mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
+ mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
+ mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
mkCoercion coCon args = ASSERT( tyConArity coCon == length args )
TyConApp coCon args
--- | Apply a 'Coercion' to another 'Coercion', which is presumably a 'Coercion' constructor of some
--- kind
+-- | Apply a 'Coercion' to another 'Coercion', which is presumably a
+-- 'Coercion' constructor of some kind
mkAppCoercion :: Coercion -> Coercion -> Coercion
-mkAppCoercion co1 co2 = mkAppTy co1 co2
+mkAppCoercion co1 co2 = mkAppTy co1 co2
-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
-- See also 'mkAppCoercion'
mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
-mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
+mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
+
+-- | Apply a type constructor to a list of coercions.
+mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
+mkTyConCoercion con cos = mkTyConApp con cos
+
+-- | Make a function 'Coercion' between two other 'Coercion's
+mkFunCoercion :: Coercion -> Coercion -> Coercion
+mkFunCoercion co1 co2 = mkFunTy co1 co2
-- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
mkForAllCoercion :: Var -> Coercion -> Coercion
-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
mkForAllCoercion tv co = ASSERT ( isTyVar tv ) mkForAllTy tv co
--- | Make a function 'Coercion' between two other 'Coercion's
-mkFunCoercion :: Coercion -> Coercion -> Coercion
-mkFunCoercion co1 co2 = mkFunTy co1 co2
-
-------------------------------
mkSymCoercion :: Coercion -> Coercion
--- ^ Create a symmetric version of the given 'Coercion' that asserts equality between
--- the same types but in the other "direction", so a kind of @t1 ~ t2@ becomes the
--- kind @t2 ~ t1@.
+-- ^ Create a symmetric version of the given 'Coercion' that asserts equality
+-- between the same types but in the other "direction", so a kind of @t1 ~ t2@
+-- becomes the kind @t2 ~ t1@.
--
--- 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
--- @sym (sym co) = co@.
+-- 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 @sym (sym co) = co@.
mkSymCoercion co
| Just co' <- coreView co = mkSymCoercion co'