mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
-
- mkCoVarCoercion,
+
+ mkClassPPredCo, mkIParamPredCo,
+ mkCoVarCoercion, mkCoPredCo,
unsafeCoercionTyCon, symCoercionTyCon,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
mkForAllTyCoI,
fromCoI,
- mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
+ mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI
) where
where
co_var = mkWildCoVar (mkCoKind s t)
+mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion
+-- Creates a coercion between (s1~t1) => r1 and (s2~t2) => r2
+mkCoPredCo = mkCoPredTy
+
+
splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
splitCoPredTy_maybe ty
| Just (cv,r) <- splitForAllTy_maybe ty
-- | Make a function 'Coercion' between two other 'Coercion's
mkFunCoercion :: Coercion -> Coercion -> Coercion
-mkFunCoercion co1 co2 = mkFunTy co1 co2
+mkFunCoercion co1 co2 = mkFunTy co1 co2 -- NB: Handles correctly the forall for eqpreds!
-- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
mkForAllCoercion :: Var -> Coercion -> Coercion
desc = CoAxiom { co_ax_tvs = tvs
, co_ax_lhs = mkTyConApp family inst_tys
, co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
+
+
+mkClassPPredCo :: Class -> [Coercion] -> Coercion
+mkClassPPredCo cls = (PredTy . ClassP cls)
+
+mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion
+mkIParamPredCo ipn = (PredTy . IParam ipn)
+
+
+
\end{code}
-- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
+
+mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI
+mkCoPredCoI coi1 coi2 coi3 = mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3
+
+
\end{code}
%************************************************************************