+lintInCo :: InCoercion -> LintM OutCoercion
+-- Check the coercion, and apply the substitution to it
+-- See Note [Linting type lets]
+lintInCo co
+ = addLoc (InCo co) $
+ do { co' <- applySubstCo co
+ ; _ <- lintCoercion co'
+ ; return co' }
+
+-------------------
+lintKind :: Kind -> LintM ()
+-- Check well-formedness of kinds: *, *->*, etc
+lintKind (TyConApp tc [])
+ | getUnique tc `elem` kindKeys
+ = return ()
+lintKind (FunTy k1 k2)
+ = lintKind k1 >> lintKind k2
+lintKind kind
+ = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
+
+-------------------
+lintTyBndrKind :: OutTyVar -> LintM ()
+lintTyBndrKind tv = lintKind (tyVarKind tv)
+
+-------------------
+lintCoercion :: OutCoercion -> LintM (OutType, OutType)
+-- Check the kind of a coercion term, returning the kind
+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 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) }
+
+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)
+ | otherwise
+ = failWithL (hang (ptext (sLit "Bad getNth:") <+> ppr co)
+ 2 (ptext (sLit "Offending type:") <+> ppr ty))
+
+-------------------
+lintType :: OutType -> LintM Kind
+lintType (TyVarTy tv)
+ = do { checkTyCoVarInScope tv
+ ; return (tyVarKind tv) }
+
+lintType ty@(AppTy t1 t2)
+ = do { k1 <- lintType t1
+ ; lint_ty_app ty k1 [t2] }
+
+lintType ty@(FunTy t1 t2)
+ = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
+
+lintType ty@(TyConApp tc tys)
+ | tyConHasKind tc
+ = lint_ty_app ty (tyConKind tc) tys
+ | otherwise
+ = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
+
+lintType (ForAllTy tv ty)
+ = do { lintTyBndrKind tv
+ ; addInScopeVar tv (lintType ty) }
+
+lintType ty@(PredTy (ClassP cls tys))
+ = lint_ty_app ty (tyConKind (classTyCon cls)) tys
+
+lintType (PredTy (IParam _ p_ty))
+ = lintType p_ty
+
+lintType ty@(PredTy (EqPred t1 t2))
+ = do { k1 <- lintType t1
+ ; k2 <- lintType t2
+ ; unless (k1 `eqKind` k2)
+ (addErrL (sep [ ptext (sLit "Kind mis-match in equality predicate:")
+ , nest 2 (ppr ty) ]))
+ ; return unliftedTypeKind }
+
+----------------
+lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
+lint_ty_app ty k tys
+ = do { ks <- mapM lintType tys
+ ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
+
+----------------
+check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
+check_co_app ty k tys
+ = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
+ k (map typeKind tys)
+ ; return () }
+
+----------------
+lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
+lint_kind_app doc kfn ks = go kfn ks
+ where
+ fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
+ nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
+ nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
+
+ go kfn [] = return kfn
+ go kfn (k:ks) = case splitKindFunTy_maybe kfn of
+ Nothing -> failWithL fail_msg
+ Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
+ (addErrL fail_msg)
+ ; go kfb ks }
+\end{code}