transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
+ -- Comparison
+ coreEqCoercion,
+
-- CoercionI
CoercionI(..),
isIdentityCoercion,
mkSymCoI, mkTransCoI,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
- mkNoteTyCoI, mkForAllTyCoI,
+ mkForAllTyCoI,
fromCoI, fromACo,
mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
coercionKind (ForAllTy tv ty)
= let (ty1, ty2) = coercionKind ty in
(ForAllTy tv ty1, ForAllTy tv ty2)
-coercionKind (NoteTy _ ty) = coercionKind ty
coercionKind (PredTy (EqPred c1 c2))
= let k1 = coercionKindPredTy c1
k2 = coercionKindPredTy c2 in
-- This case handled by coreView
splitNewTypeRepCo_maybe _
= Nothing
+
+-------------------------------------
+-- Syntactic equality of coercions
+
+coreEqCoercion :: Coercion -> Coercion -> Bool
+coreEqCoercion = coreEqType
\end{code}
mkFunTyCoI ty1 coi1 ty2 coi2 =
ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2)
-mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI
-mkNoteTyCoI _ IdCo = IdCo
-mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co
-
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
mkForAllTyCoI _ IdCo = IdCo
mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co