; (s,t) <- addInScopeVar v (lintCoercion co)
; return (ForAllTy v s, ForAllTy v t) }
-lintCoercion co@(PredCo (ClassP cls cos))
- = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
- ; check_co_app co (tyConKind (classTyCon cls)) ss
- ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
-
-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) }
= lint_ty_app ty (tyConKind funTyCon) [t1,t2]
lintType ty@(TyConApp tc tys)
+ | tc `hasKey` eqPredPrimTyConKey -- See Note [The (~) TyCon] in TysPrim
+ = lint_eq_pred ty tys
| tyConHasKind tc
= lint_ty_app ty (tyConKind tc) tys
| otherwise
lint_ty_app ty k tys
= do { ks <- mapM lintType tys
; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
-
+
+lint_eq_pred :: Type -> [OutType] -> LintM Kind
+lint_eq_pred ty arg_tys
+ | [ty1,ty2] <- arg_tys
+ = do { k1 <- lintType ty1
+ ; k2 <- lintType ty2
+ ; checkL (k1 `eqKind` k2)
+ (ptext (sLit "Mismatched arg kinds:") <+> ppr ty)
+ ; return unliftedTypeKind }
+ | otherwise
+ = failWithL (ptext (sLit "Unsaturated (~) type") <+> ppr ty)
+
----------------
check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
check_co_app ty k tys