-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 (PredCo (IParam ip co))
+ = do { (s,t) <- lintCoercion co
+ ; return (PredTy (IParam ip s), PredTy (IParam ip t)) }
+
+lintCoercion (PredCo (EqPred c1 c2))
+ = do { (s1,t1) <- lintCoercion c1
+ ; (s2,t2) <- lintCoercion c2
+ ; return (PredTy (EqPred s1 s2), PredTy (EqPred t1 t2)) }
+
+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)