+-------------------
+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
+ | isCoVar tv = lintCoVarKind tv
+ | otherwise = lintKind (tyVarKind tv)
+
+-------------------
+lintCoVarKind :: OutCoVar -> LintM ()
+-- Check the kind of a coercion binder
+lintCoVarKind tv
+ = do { (ty1,ty2) <- lintSplitCoVar tv
+ ; k1 <- lintType ty1
+ ; k2 <- lintType ty2
+ ; unless (k1 `eqKind` k2)
+ (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
+ , nest 2 (quotes (ppr tv))
+ , ppr [k1,k2] ])) }
+
+-------------------
+lintSplitCoVar :: CoVar -> LintM (Type,Type)
+lintSplitCoVar cv
+ = case coVarKind_maybe cv of
+ Just ts -> return ts
+ Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
+ , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
+
+-------------------
+lintCoercion :: OutType -> LintM (OutType, OutType)
+-- Check the kind of a coercion term, returning the kind
+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) }
+
+ | 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))
+
+-------------------
+lintType :: OutType -> LintM Kind
+lintType (TyVarTy tv)
+ = do { checkTyVarInScope 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 {}))
+ = failWithL (badEq ty)
+
+----------------
+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 }
+--------------
+badEq :: Type -> SDoc
+badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
+ 1 (quotes (ppr ty))
+\end{code}