mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
-
- mkCoVarCoercion,
+
+ mkClassPPredCo, mkIParamPredCo, mkEqPredCo,
+ mkCoVarCoercion, mkCoPredCo,
unsafeCoercionTyCon, symCoercionTyCon,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
mkForAllTyCoI,
fromCoI,
- mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
+ mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI
) where
import Class
import Var
import VarEnv
+import VarSet
import Name
import PrelNames
import Util
-- | (mkCoPredTy s t r) produces the type: (s~t) => r
mkCoPredTy :: Type -> Type -> Type -> Type
-mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r
+mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) )
+ ForAllTy co_var r
+ 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
-- | 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)
+
+mkEqPredCo :: Coercion -> Coercion -> Coercion
+mkEqPredCo co1 co2 = PredTy (EqPred co1 co2)
+
+
\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}
%************************************************************************
--
-- > c :: (t1 ~ t2)
--
--- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@.
+-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@,
+-- then @coercionKind c = (t1, t2)@.
coercionKind :: Coercion -> (Type, Type)
coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
| otherwise = (ty, ty)
= (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty)
where
(tys1, tys2) = coercionKinds cos
-coTyConAppKind desc cos = pprPanic "coTyConAppKind" (ppr desc $$ ppr cos)
+coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat
+ [ ppr co <+> dcolon <+> pprEqPred (coercionKind co)
+ | co <- cos ])) $
+ coercionKind (head cos)
\end{code}