-lintCoercion ty@(TyVarTy tv)
- = do { checkTyVarInScope tv
- ; if isCoVar tv then return (coVarKind tv)
- else return (ty, ty) }
-
-lintCoercion ty@(AppTy ty1 ty2)
- = do { (s1,t1) <- lintCoercion ty1
- ; (s2,t2) <- lintCoercion ty2
- ; check_co_app ty (typeKind s1) [s2]
- ; return (AppTy s1 s2, AppTy t1 t2) }
-
-lintCoercion ty@(FunTy ty1 ty2)
- = do { (s1,t1) <- lintCoercion ty1
- ; (s2,t2) <- lintCoercion ty2
- ; check_co_app ty (tyConKind funTyCon) [s1, s2]
- ; return (FunTy s1 s2, FunTy t1 t2) }
-
-lintCoercion ty@(TyConApp tc tys)
- | Just (ar, desc) <- isCoercionTyCon_maybe tc
- = do { unless (tys `lengthAtLeast` ar) (badCo ty)
- ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
- ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
- ; check_co_app ty (typeKind s) ss
- ; return (mkAppTys s ss, mkAppTys t ts) }
-
- | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon
- = badCo ty
-
- | otherwise
- = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
- ; check_co_app ty (tyConKind tc) ss
- ; return (TyConApp tc ss, TyConApp tc ts) }
-
-lintCoercion ty@(PredTy (ClassP cls tys))
- = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
- ; check_co_app ty (tyConKind (classTyCon cls)) ss
- ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
-
-lintCoercion (PredTy (IParam n p_ty))
- = do { (s,t) <- lintCoercion p_ty
- ; return (PredTy (IParam n s), PredTy (IParam n t)) }
-
-lintCoercion ty@(PredTy (EqPred {}))
- = failWithL (badEq ty)
-
-lintCoercion (ForAllTy tv ty)
- | isCoVar tv
- = do { (co1, co2) <- lintSplitCoVar tv
- ; (s1,t1) <- lintCoercion co1
- ; (s2,t2) <- lintCoercion co2
- ; (sr,tr) <- lintCoercion ty
- ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
-
- | otherwise
- = do { lintKind (tyVarKind tv)
- ; (s,t) <- addInScopeVar tv (lintCoercion ty)
- ; return (ForAllTy tv s, ForAllTy tv t) }
-
-badCo :: Coercion -> LintM a
-badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
-
----------------
-lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
--- Always called with correct number of coercion arguments
--- First arg is just for error message
-lintCoTyConApp _ CoLeft (co:_) = lintLR fst co
-lintCoTyConApp _ CoRight (co:_) = lintLR snd co
-lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3 co
-lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3 co
-lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
-
-lintCoTyConApp _ CoSym (co:_)
- = do { (ty1,ty2) <- lintCoercion co
- ; return (ty2,ty1) }
-
-lintCoTyConApp co CoTrans (co1:co2:_)
+lintCoercion (Refl ty)
+ = do { ty' <- lintInTy ty
+ ; return (ty', ty') }
+
+lintCoercion co@(TyConAppCo tc cos)
+ = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
+ ; check_co_app co (tyConKind tc) ss
+ ; return (mkTyConApp tc ss, mkTyConApp tc ts) }
+
+lintCoercion co@(AppCo co1 co2)
+ = do { (s1,t1) <- lintCoercion co1
+ ; (s2,t2) <- lintCoercion co2
+ ; check_co_app co (typeKind s1) [s2]
+ ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
+
+lintCoercion (ForAllCo v co)
+ = do { lintKind (tyVarKind v)
+ ; (s,t) <- addInScopeVar v (lintCoercion co)
+ ; return (ForAllTy v s, ForAllTy v t) }
+
+lintCoercion (CoVarCo cv)
+ = do { checkTyCoVarInScope cv
+ ; return (coVarKind cv) }
+
+lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = tvs
+ , co_ax_lhs = lhs
+ , co_ax_rhs = rhs })
+ cos)
+ = do { (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs cos)
+ ; return (substTyWith tvs tys1 lhs,
+ substTyWith tvs tys2 rhs) }
+
+lintCoercion (UnsafeCo ty1 ty2)
+ = do { ty1' <- lintInTy ty1
+ ; ty2' <- lintInTy ty2
+ ; return (ty1', ty2') }
+
+lintCoercion (SymCo co)
+ = do { (ty1, ty2) <- lintCoercion co
+ ; return (ty2, ty1) }
+
+lintCoercion co@(TransCo co1 co2)