-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, rule) <- isCoercionTyCon_maybe tc
- = do { unless (tys `lengthAtLeast` ar) (badCo ty)
- ; (s,t) <- rule lintType lintCoercion
- True (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) }
-
+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)
+ = do { (ty1a, ty1b) <- lintCoercion co1
+ ; (ty2a, ty2b) <- lintCoercion co2
+ ; checkL (ty1b `eqType` ty2a)
+ (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
+ 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
+ ; return (ty1a, ty2b) }
+
+lintCoercion the_co@(NthCo d co)
+ = do { (s,t) <- lintCoercion co
+ ; sn <- checkTcApp the_co d s
+ ; tn <- checkTcApp the_co d t
+ ; return (sn, tn) }
+
+lintCoercion (InstCo co arg_ty)
+ = do { co_tys <- lintCoercion co
+ ; arg_kind <- lintType arg_ty
+ ; case splitForAllTy_maybe `traverse` toPair co_tys of
+ Just (Pair (tv1,ty1) (tv2,ty2))
+ | arg_kind `isSubKind` tyVarKind tv1
+ -> return (substTyWith [tv1] [arg_ty] ty1,
+ substTyWith [tv2] [arg_ty] ty2)
+ | otherwise
+ -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
+ Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
+
+----------
+checkTcApp :: Coercion -> Int -> Type -> LintM Type
+checkTcApp co n ty
+ | Just (_, tys) <- splitTyConApp_maybe ty
+ , n < length tys
+ = return (tys !! n)