+
+-------------- DEAD CODE -------------------
+
+-------------------
+checkCoKind :: CoVar -> OutCoercion -> LintM ()
+-- Both args have had substitution applied
+checkCoKind covar arg_co
+ = do { (s2,t2) <- lintCoercion arg_co
+ ; unless (s1 `eqType` s2 && t1 `coreEqType` t2)
+ (addErrL (mkCoAppErrMsg covar arg_co)) }
+ where
+ (s1,t1) = coVarKind covar
+
+lintCoVarKind :: OutCoVar -> LintM ()
+-- Check the kind of a coercion binder
+lintCoVarKind tv
+ = do { (ty1,ty2) <- lintSplitCoVar tv
+ ; lintEqType ty1 ty2
+
+
+-------------------
+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))])
+
+mkCoVarLetErr :: CoVar -> Coercion -> Message
+mkCoVarLetErr covar co
+ = vcat [ptext (sLit "Bad `let' binding for coercion variable:"),
+ hang (ptext (sLit "Coercion variable:"))
+ 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
+ hang (ptext (sLit "Arg coercion:"))
+ 4 (ppr co)]
+
+mkCoAppErrMsg :: CoVar -> Coercion -> Message
+mkCoAppErrMsg covar arg_co
+ = vcat [ptext (sLit "Kinds don't match in coercion application:"),
+ hang (ptext (sLit "Coercion variable:"))
+ 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
+ hang (ptext (sLit "Arg coercion:"))
+ 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
+
+
+mkCoAppMsg :: Type -> Coercion -> Message
+mkCoAppMsg ty arg_co
+ = vcat [text "Illegal type application:",
+ hang (ptext (sLit "exp type:"))
+ 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
+ hang (ptext (sLit "arg type:"))
+ 4 (ppr arg_co <+> dcolon <+> ppr (coercionKind arg_co))]
+