Print which warning-flag controls an emitted warning
[ghc.git] / compiler / coreSyn / CoreLint.hs
index 41b6a94..f5d0f84 100644 (file)
@@ -7,7 +7,6 @@ A ``lint'' pass to check for Core correctness
 -}
 
 {-# LANGUAGE CPP #-}
-{-# OPTIONS_GHC -fprof-auto #-}
 
 module CoreLint (
     lintCoreBindings, lintUnfolding,
@@ -25,12 +24,13 @@ module CoreLint (
 import CoreSyn
 import CoreFVs
 import CoreUtils
+import CoreStats   ( coreBindsStats )
 import CoreMonad
 import Bag
 import Literal
 import DataCon
 import TysWiredIn
-import TysPrim
+import TcType ( isFloatingTy )
 import Var
 import VarEnv
 import VarSet
@@ -42,7 +42,7 @@ import Coercion
 import SrcLoc
 import Kind
 import Type
-import TypeRep
+import TyCoRep       -- checks validity of types/coercions
 import TyCon
 import CoAxiom
 import BasicTypes
@@ -62,6 +62,9 @@ import Demand ( splitStrictSig, isBotRes )
 import HscTypes
 import DynFlags
 import Control.Monad
+#if __GLASGOW_HASKELL__ > 710
+import qualified Control.Monad.Fail as MonadFail
+#endif
 import MonadUtils
 import Data.Maybe
 import Pair
@@ -73,12 +76,30 @@ This file implements the type-checking algorithm for System FC, the "official"
 name of the Core language. Type safety of FC is heart of the claim that
 executables produced by GHC do not have segmentation faults. Thus, it is
 useful to be able to reason about System FC independently of reading the code.
-To this purpose, there is a document ghc.pdf built in docs/core-spec that
+To this purpose, there is a document core-spec.pdf built in docs/core-spec that
 contains a formalism of the types and functions dealt with here. If you change
 just about anything in this file or you change other types/functions throughout
 the Core language (all signposted to this note), you should update that
 formalism. See docs/core-spec/README for more info about how to do so.
 
+Note [check vs lint]
+~~~~~~~~~~~~~~~~~~~~
+This file implements both a type checking algorithm and also general sanity
+checking. For example, the "sanity checking" checks for TyConApp on the left
+of an AppTy, which should never happen. These sanity checks don't really
+affect any notion of type soundness. Yet, it is convenient to do the sanity
+checks at the same time as the type checks. So, we use the following naming
+convention:
+
+- Functions that begin with 'lint'... are involved in type checking. These
+  functions might also do some sanity checking.
+
+- Functions that begin with 'check'... are *not* involved in type checking.
+  They exist only for sanity checking.
+
+Issues surrounding variable naming, shadowing, and such are considered *not*
+to be part of type checking, as the formalism omits these details.
+
 Summary of checks
 ~~~~~~~~~~~~~~~~~
 Checks that a set of core bindings is well-formed.  The PprStyle and String
@@ -115,14 +136,14 @@ That is, use a type let.   See Note [Type let] in CoreSyn.
 However, when linting <body> we need to remember that a=Int, else we might
 reject a correct program.  So we carry a type substitution (in this example
 [a -> Int]) and apply this substitution before comparing types.  The functin
-        lintInTy :: Type -> LintM Type
-returns a substituted type; that's the only reason it returns anything.
+        lintInTy :: Type -> LintM (Type, Kind)
+returns a substituted type.
 
 When we encounter a binder (like x::a) we must apply the substitution
 to the type of the binding variable.  lintBinders does this.
 
 For Ids, the type-substituted Id is added to the in_scope set (which
-itself is part of the TvSubst we are carrying down), and when we
+itself is part of the TCvSubst we are carrying down), and when we
 find an occurrence of an Id, we fetch it from the in-scope set.
 
 Note [Bad unsafe coercion]
@@ -209,10 +230,10 @@ dumpPassResult dflags unqual mb_flag hdr extra_info binds rules
     dump_doc  = vcat [ nest 2 extra_info
                      , size_doc
                      , blankLine
-                     , pprCoreBindings binds
+                     , pprCoreBindingsWithSize binds
                      , ppUnless (null rules) pp_rules ]
     pp_rules = vcat [ blankLine
-                    , ptext (sLit "------ Local rules for imported ids --------")
+                    , text "------ Local rules for imported ids --------"
                     , pprRules rules ]
 
 coreDumpFlag :: CoreToDo -> Maybe DumpFlag
@@ -263,26 +284,26 @@ displayLintResults :: DynFlags -> CoreToDo
                    -> IO ()
 displayLintResults dflags pass warns errs binds
   | not (isEmptyBag errs)
-  = do { log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
+  = do { log_action dflags dflags NoReason Err.SevDump noSrcSpan defaultDumpStyle
            (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs
-                 , ptext (sLit "*** Offending Program ***")
+                 , text "*** Offending Program ***"
                  , pprCoreBindings binds
-                 , ptext (sLit "*** End of Offense ***") ])
+                 , text "*** End of Offense ***" ])
        ; Err.ghcExit dflags 1 }
 
   | not (isEmptyBag warns)
   , not opt_NoDebugOutput
   , showLintWarnings pass
-  = log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
+  = log_action dflags dflags NoReason Err.SevDump noSrcSpan defaultDumpStyle
         (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag warns)
 
   | otherwise = return ()
   where
 
 lint_banner :: String -> SDoc -> SDoc
-lint_banner string pass = ptext (sLit "*** Core Lint")      <+> text string
-                          <+> ptext (sLit ": in result of") <+> pass
-                          <+> ptext (sLit "***")
+lint_banner string pass = text "*** Core Lint"      <+> text string
+                          <+> text ": in result of" <+> pass
+                          <+> text "***"
 
 showLintWarnings :: CoreToDo -> Bool
 -- Disable Lint warnings on the first simplifier pass, because
@@ -303,12 +324,13 @@ lintInteractiveExpr what hsc_env expr
     dflags = hsc_dflags hsc_env
 
     display_lint_err err
-      = do { log_action dflags dflags Err.SevDump noSrcSpan defaultDumpStyle
+      = do { log_action dflags dflags NoReason Err.SevDump
+               noSrcSpan defaultDumpStyle
                (vcat [ lint_banner "errors" (text what)
                      , err
-                     , ptext (sLit "*** Offending Program ***")
+                     , text "*** Offending Program ***"
                      , pprCoreExpr expr
-                     , ptext (sLit "*** End of Offense ***") ])
+                     , text "*** End of Offense ***" ])
            ; Err.ghcExit dflags 1 }
 
 interactiveInScope :: HscEnv -> [Var]
@@ -332,7 +354,7 @@ interactiveInScope hsc_env
     te1    = mkTypeEnvWithImplicits (ic_tythings ictxt)
     te     = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
     ids    = typeEnvIds te
-    tyvars = mapUnionVarSet (tyVarsOfType . idType) ids
+    tyvars = mapUnionVarSet (tyCoVarsOfType . idType) ids
               -- Why the type variables?  How can the top level envt have free tyvars?
               -- I think it's because of the GHCi debugger, which can bind variables
               --   f :: [t] -> [t]
@@ -448,11 +470,11 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
     do { ty <- lintCoreExpr rhs
        ; lintBinder binder -- Check match to RHS type
        ; binder_ty <- applySubstTy (idType binder)
-       ; checkTys binder_ty ty (mkRhsMsg binder (ptext (sLit "RHS")) ty)
+       ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
 
         -- Check the let/app invariant
         -- See Note [CoreSyn let/app invariant] in CoreSyn
-       ; checkL (not (isUnLiftedType binder_ty)
+       ; checkL (not (isUnliftedType binder_ty)
             || (isNonRec rec_flag && exprOkForSpeculation rhs))
            (mkRhsPrimMsg binder rhs)
 
@@ -473,7 +495,7 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
        ; when (lf_check_inline_loop_breakers flags
                && isStrongLoopBreaker (idOccInfo binder)
                && isInlinePragma (idInlinePragma binder))
-              (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
+              (addWarnL (text "INLINE binder is (non-rule) loop breaker:" <+> ppr binder))
               -- Only non-rule loop breakers inhibit inlining
 
       -- Check whether arity and demand type are consistent (only if demand analysis
@@ -490,16 +512,16 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
        -- the type and the strictness signature. See Note [exprArity invariant]
        -- and Note [Trimming arity]
        ; checkL (idArity binder <= length (typeArity (idType binder)))
-           (ptext (sLit "idArity") <+> ppr (idArity binder) <+>
-           ptext (sLit "exceeds typeArity") <+>
+           (text "idArity" <+> ppr (idArity binder) <+>
+           text "exceeds typeArity" <+>
            ppr (length (typeArity (idType binder))) <> colon <+>
            ppr binder)
 
        ; case splitStrictSig (idStrictness binder) of
            (demands, result_info) | isBotRes result_info ->
              checkL (idArity binder <= length demands)
-               (ptext (sLit "idArity") <+> ppr (idArity binder) <+>
-               ptext (sLit "exceeds arity imposed by the strictness signature") <+>
+               (text "idArity" <+> ppr (idArity binder) <+>
+               text "exceeds arity imposed by the strictness signature" <+>
                ppr (idStrictness binder) <> colon <+>
                ppr binder)
            _ -> return ()
@@ -519,9 +541,9 @@ lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
 lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
   | isStableSource src
   = do { ty <- lintCoreExpr rhs
-       ; checkTys bndr_ty ty (mkRhsMsg bndr (ptext (sLit "unfolding")) ty) }
+       ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
 lintIdUnfolding  _ _ _
-  = return ()       -- Do not Lint unstable unfoldings, becuase that leads
+  = return ()       -- Do not Lint unstable unfoldings, because that leads
                     -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars
 
 {-
@@ -541,24 +563,23 @@ the desugarer.
 ************************************************************************
 -}
 
---type InKind      = Kind       -- Substitution not yet applied
 type InType      = Type
 type InCoercion  = Coercion
 type InVar       = Var
-type InTyVar     = TyVar
-
-type OutKind     = Kind -- Substitution has been applied to this,
-                        -- but has not been linted yet
-type LintedKind  = Kind -- Substitution applied, and type is linted
+type InTyVar     = Var
+type InCoVar     = Var
 
 type OutType     = Type -- Substitution has been applied to this,
                         -- but has not been linted yet
+type OutKind     = Kind
 
 type LintedType  = Type -- Substitution applied, and type is linted
+type LintedKind  = Kind
 
-type OutCoercion = Coercion
-type OutVar      = Var
-type OutTyVar    = TyVar
+type OutCoercion    = Coercion
+type OutVar         = Var
+type OutTyVar       = TyVar
+type OutCoVar       = Var
 
 lintCoreExpr :: CoreExpr -> LintM OutType
 -- The returned type has the substitution from the monad
@@ -571,10 +592,10 @@ lintCoreExpr :: CoreExpr -> LintM OutType
 -- See Note [GHC Formalism]
 lintCoreExpr (Var var)
   = do  { checkL (not (var == oneTupleDataConId))
-                 (ptext (sLit "Illegal one-tuple"))
+                 (text "Illegal one-tuple")
 
         ; checkL (isId var && not (isCoVar var))
-                 (ptext (sLit "Non term variable") <+> ppr var)
+                 (text "Non term variable" <+> ppr var)
 
         ; checkDeadIdOcc var
         ; var' <- lookupIdInScope var
@@ -586,9 +607,11 @@ lintCoreExpr (Lit lit)
 lintCoreExpr (Cast expr co)
   = do { expr_ty <- lintCoreExpr expr
        ; co' <- applySubstCo co
-       ; (_, from_ty, to_ty, r) <- lintCoercion co'
-       ; checkRole co' Representational r
-       ; checkTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
+       ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
+       ; lintL (classifiesTypeWithValues k2)
+               (text "Target of cast not # or *:" <+> ppr co)
+       ; lintRole co' Representational r
+       ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
        ; return to_ty }
 
 lintCoreExpr (Tick (Breakpoint _ ids) expr)
@@ -605,7 +628,7 @@ lintCoreExpr (Let (NonRec tv (Type ty)) body)
   =     -- See Note [Linting type lets]
     do  { ty' <- applySubstTy ty
         ; lintTyBndr tv              $ \ tv' ->
-    do  { addLoc (RhsOf tv) $ checkTyKind tv' ty'
+    do  { addLoc (RhsOf tv) $ lintTyKind tv' ty'
                 -- Now extend the substitution so we
                 -- take advantage of it in the body
         ; extendSubstL tv' ty'       $
@@ -640,27 +663,31 @@ lintCoreExpr (Lam var expr)
   = addLoc (LambdaBodyOf var) $
     lintBinder var $ \ var' ->
     do { body_ty <- lintCoreExpr expr
-       ; if isId var' then
-             return (mkFunTy (idType var') body_ty)
-         else
-             return (mkForAllTy var' body_ty)
-       }
-        -- The applySubstTy is needed to apply the subst to var
+       ; return $ mkPiType var' body_ty }
 
 lintCoreExpr e@(Case scrut var alt_ty alts) =
        -- Check the scrutinee
   do { scrut_ty <- lintCoreExpr scrut
-     ; alt_ty   <- lintInTy alt_ty
-     ; var_ty   <- lintInTy (idType var)
+     ; (alt_ty, _) <- lintInTy alt_ty
+     ; (var_ty, _) <- lintInTy (idType var)
 
      -- See Note [No alternatives lint check]
      ; when (null alts) $
      do { checkL (not (exprIsHNF scrut))
-          (ptext (sLit "No alternatives for a case scrutinee in head-normal form:") <+> ppr scrut)
+          (text "No alternatives for a case scrutinee in head-normal form:" <+> ppr scrut)
         ; checkL (exprIsBottom scrut)
-          (ptext (sLit "No alternatives for a case scrutinee not known to diverge for sure:") <+> ppr scrut)
+          (text "No alternatives for a case scrutinee not known to diverge for sure:" <+> ppr scrut)
         }
 
+     -- See Note [Rules for floating-point comparisons] in PrelRules
+     ; let isLitPat (LitAlt _, _ , _) = True
+           isLitPat _                 = False
+     ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
+         (ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
+                        "expression with literal pattern in case " ++
+                        "analysis (see Trac #9238).")
+          $$ text "scrut" <+> ppr scrut)
+
      ; case tyConAppTyCon_maybe (idType var) of
          Just tycon
               | debugIsOn &&
@@ -674,8 +701,8 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
 
         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
 
-     ; subst <- getTvSubst
-     ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
+     ; subst <- getTCvSubst
+     ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
 
      ; lintAndScopeId var $ \_ ->
        do { -- Check the alternatives
@@ -686,32 +713,13 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
 -- This case can't happen; linting types in expressions gets routed through
 -- lintCoreArgs
 lintCoreExpr (Type ty)
-  = failWithL (ptext (sLit "Type found as expression") <+> ppr ty)
+  = failWithL (text "Type found as expression" <+> ppr ty)
 
 lintCoreExpr (Coercion co)
-  = do { (_kind, ty1, ty2, role) <- lintInCo co
-       ; return (mkCoercionType role ty1 ty2) }
+  = do { (k1, k2, ty1, ty2, role) <- lintInCo co
+       ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
 
 {-
-Note [Kind instantiation in coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following coercion axiom:
-  ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa
-
-Consider the following instantiation:
-  ax_co <* -> *> <Monad>
-
-We need to split the co_ax_tvs into kind and type variables in order
-to find out the coercion kind instantiations. Those can only be Refl
-since we don't have kind coercions. This is just a way to represent
-kind instantiation.
-
-We use the number of kind variables to know how to split the coercions
-instantiations between kind coercions and type coercions. We lint the
-kind coercions and produce the following substitution which is to be
-applied in the type variables:
-  k_ag   ~~>   * -> *
-
 Note [No alternatives lint check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Case expressions with no alternatives are odd beasts, and worth looking at
@@ -744,12 +752,15 @@ subtype of the required type, as one would expect.
 
 lintCoreArg  :: OutType -> CoreArg -> LintM OutType
 lintCoreArg fun_ty (Type arg_ty)
-  = do { arg_ty' <- applySubstTy arg_ty
+  = do { checkL (not (isCoercionTy arg_ty))
+                (text "Unnecessary coercion-to-type injection:"
+                  <+> ppr arg_ty)
+       ; arg_ty' <- applySubstTy arg_ty
        ; lintTyApp fun_ty arg_ty' }
 
 lintCoreArg fun_ty arg
   = do { arg_ty <- lintCoreExpr arg
-       ; checkL (not (isUnLiftedType arg_ty) || exprOkForSpeculation arg)
+       ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
                 (mkLetAppMsg arg)
        ; lintValApp arg fun_ty arg_ty }
 
@@ -761,7 +772,7 @@ lintAltBinders :: OutType     -- Scrutinee type
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintAltBinders scrut_ty con_ty []
-  = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
+  = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
 lintAltBinders scrut_ty con_ty (bndr:bndrs)
   | isTyVar bndr
   = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
@@ -773,10 +784,13 @@ lintAltBinders scrut_ty con_ty (bndr:bndrs)
 -----------------
 lintTyApp :: OutType -> OutType -> LintM OutType
 lintTyApp fun_ty arg_ty
-  | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
-  , isTyVar tyvar
-  = do  { checkTyKind tyvar arg_ty
-        ; return (substTyWith [tyvar] [arg_ty] body_ty) }
+  | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
+  = do  { lintTyKind tv arg_ty
+        ; in_scope <- getInScope
+        -- substTy needs the set of tyvars in scope to avoid generating
+        -- uniques that are already in scope.
+        -- See Note [The substitution invariant] in TyCoRep
+        ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
 
   | otherwise
   = failWithL (mkTyAppMsg fun_ty arg_ty)
@@ -785,7 +799,7 @@ lintTyApp fun_ty arg_ty
 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
 lintValApp arg fun_ty arg_ty
   | Just (arg,res) <- splitFunTy_maybe fun_ty
-  = do { checkTys arg arg_ty err1
+  = do { ensureEqTys arg arg_ty err1
        ; return res }
   | otherwise
   = failWithL err2
@@ -793,21 +807,18 @@ lintValApp arg fun_ty arg_ty
     err1 = mkAppMsg       fun_ty arg_ty arg
     err2 = mkNonFunAppMsg fun_ty arg_ty arg
 
-checkTyKind :: OutTyVar -> OutType -> LintM ()
+lintTyKind :: OutTyVar -> OutType -> LintM ()
 -- Both args have had substitution applied
 
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
-checkTyKind tyvar arg_ty
-  | isSuperKind tyvar_kind  -- kind forall
-  = lintKind arg_ty
+lintTyKind tyvar arg_ty
         -- Arg type might be boxed for a function with an uncommitted
         -- tyvar; notably this is used so that we can give
         --      error :: forall a:*. String -> a
         -- and then apply it to both boxed and unboxed types.
-  | otherwise  -- type forall
   = do { arg_kind <- lintType arg_ty
-       ; unless (arg_kind `isSubKind` tyvar_kind)
+       ; unless (arg_kind `eqType` tyvar_kind)
                 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
   where
     tyvar_kind = tyVarKind tyvar
@@ -819,7 +830,7 @@ checkDeadIdOcc id
   | isDeadOcc (idOccInfo id)
   = do { in_case <- inCasePat
        ; checkL in_case
-                (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
+                (text "Occurrence of a dead Id" <+> ppr id) }
   | otherwise
   = return ()
 
@@ -868,10 +879,10 @@ checkCaseAlts e ty alts =
                         Nothing    -> False
                         Just tycon -> isPrimTyCon tycon
 
-checkAltExpr :: CoreExpr -> OutType -> LintM ()
-checkAltExpr expr ann_ty
+lintAltExpr :: CoreExpr -> OutType -> LintM ()
+lintAltExpr expr ann_ty
   = do { actual_ty <- lintCoreExpr expr
-       ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
+       ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
 
 lintCoreAlt :: OutType          -- Type of scrutinee
             -> OutType          -- Type of the alternative
@@ -880,16 +891,16 @@ lintCoreAlt :: OutType          -- Type of scrutinee
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
-  do { checkL (null args) (mkDefaultArgsMsg args)
-     ; checkAltExpr rhs alt_ty }
+  do { lintL (null args) (mkDefaultArgsMsg args)
+     ; lintAltExpr rhs alt_ty }
 
 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
   | litIsLifted lit
   = failWithL integerScrutinisedMsg
   | otherwise
-  = do { checkL (null args) (mkDefaultArgsMsg args)
-       ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
-       ; checkAltExpr rhs alt_ty }
+  = do { lintL (null args) (mkDefaultArgsMsg args)
+       ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
+       ; lintAltExpr rhs alt_ty }
   where
     lit_ty = literalType lit
 
@@ -901,13 +912,13 @@ lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
     {   -- First instantiate the universally quantified
         -- type variables of the data constructor
         -- We've already check
-      checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
-    ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
+      lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
+    ; let con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
 
         -- And now bring the new binders into scope
     ; lintBinders args $ \ args' -> do
     { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
-    ; checkAltExpr rhs alt_ty } }
+    ; lintAltExpr rhs alt_ty } }
 
   | otherwise   -- Scrut-ty is wrong shape
   = addErrL (mkBadAltMsg scrut_ty alt)
@@ -934,15 +945,25 @@ lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 -- See Note [GHC Formalism]
 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 lintBinder var linterF
-  | isId var  = lintIdBndr var linterF
-  | otherwise = lintTyBndr var linterF
+  | isTyVar var = lintTyBndr var linterF
+  | isCoVar var = lintCoBndr var linterF
+  | otherwise   = lintIdBndr var linterF
 
 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
 lintTyBndr tv thing_inside
-  = do { subst <- getTvSubst
-       ; let (subst', tv') = Type.substTyVarBndr subst tv
-       ; lintTyBndrKind tv'
-       ; updateTvSubst subst' (thing_inside tv') }
+  = do { subst <- getTCvSubst
+       ; let (subst', tv') = substTyVarBndr subst tv
+       ; lintKind (varType tv')
+       ; updateTCvSubst subst' (thing_inside tv') }
+
+lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a
+lintCoBndr cv thing_inside
+  = do { subst <- getTCvSubst
+       ; let (subst', cv') = substCoVarBndr subst cv
+       ; lintKind (varType cv')
+       ; lintL (isCoercionType (varType cv'))
+               (text "CoVar with non-coercion type:" <+> pprTvBndr cv)
+       ; updateTCvSubst subst' (thing_inside cv') }
 
 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
 -- Do substitution on the type of a binder and add the var with this
@@ -965,38 +986,37 @@ lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
 lintAndScopeId id linterF
   = do { flags <- getLintFlags
        ; checkL (not (lf_check_global_ids flags) || isLocalId id)
-                (ptext (sLit "Non-local Id binder") <+> ppr id)
+                (text "Non-local Id binder" <+> ppr id)
                 -- See Note [Checking for global Ids]
-       ; ty <- lintInTy (idType id)
+       ; (ty, k) <- lintInTy (idType id)
+       ; lintL (not (isRuntimeRepPolymorphic k))
+           (text "RuntimeRep-polymorphic binder:" <+>
+                 (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k)))
        ; let id' = setIdType id ty
        ; addInScopeVar id' $ (linterF id') }
 
 {-
-************************************************************************
-*                                                                      *
-             Types and kinds
-*                                                                      *
-************************************************************************
-
-We have a single linter for types and kinds.  That is convenient
-because sometimes it's not clear whether the thing we are looking
-at is a type or a kind.
+%************************************************************************
+%*                                                                      *
+             Types
+%*                                                                      *
+%************************************************************************
 -}
 
-lintInTy :: InType -> LintM LintedType
+lintInTy :: InType -> LintM (LintedType, LintedKind)
 -- Types only, not kinds
 -- Check the type, and apply the substitution to it
 -- See Note [Linting type lets]
 lintInTy ty
   = addLoc (InType ty) $
     do  { ty' <- applySubstTy ty
-        ; _k  <- lintType ty'
-        ; return ty' }
+        ; k  <- lintType ty'
+        ; lintKind k
+        ; return (ty', k) }
 
--------------------
-lintTyBndrKind :: OutTyVar -> LintM ()
--- Handles both type and kind foralls.
-lintTyBndrKind tv = lintKind (tyVarKind tv)
+checkTyCon :: TyCon -> LintM ()
+checkTyCon tc
+  = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
 
 -------------------
 lintType :: OutType -> LintM LintedKind
@@ -1005,81 +1025,107 @@ lintType :: OutType -> LintM LintedKind
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintType (TyVarTy tv)
-  = do { checkTyCoVarInScope tv
+  = do { checkL (isTyVar tv) (mkBadTyVarMsg tv)
+       ; lintTyCoVarInScope tv
        ; return (tyVarKind tv) }
          -- We checked its kind when we added it to the envt
 
 lintType ty@(AppTy t1 t2)
+  | TyConApp {} <- t1
+  = failWithL $ text "TyConApp to the left of AppTy:" <+> ppr ty
+  | otherwise
   = do { k1 <- lintType t1
        ; k2 <- lintType t2
        ; lint_ty_app ty k1 [(t2,k2)] }
 
-lintType ty@(FunTy t1 t2)    -- (->) has two different rules, for types and kinds
-  = do { k1 <- lintType t1
-       ; k2 <- lintType t2
-       ; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
-
 lintType ty@(TyConApp tc tys)
   | Just ty' <- coreView ty
   = lintType ty'   -- Expand type synonyms, so that we do not bogusly complain
                    --  about un-saturated type synonyms
 
-  | isUnLiftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
-       -- See Note [The kind invariant] in TypeRep
+  | isUnliftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
        -- Also type synonyms and type families
   , length tys < tyConArity tc
-  = failWithL (hang (ptext (sLit "Un-saturated type application")) 2 (ppr ty))
+  = failWithL (hang (text "Un-saturated type application") 2 (ppr ty))
 
   | otherwise
-  = do { ks <- mapM lintType tys
+  = do { checkTyCon tc
+       ; ks <- mapM lintType tys
        ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
 
-lintType (ForAllTy tv ty)
-  = do { lintTyBndrKind tv
-       ; addInScopeVar tv (lintType ty) }
+-- arrows can related *unlifted* kinds, so this has to be separate from
+-- a dependent forall.
+lintType ty@(ForAllTy (Anon t1) t2)
+  = do { k1 <- lintType t1
+       ; k2 <- lintType t2
+       ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
+
+lintType t@(ForAllTy (Named tv _vis) ty)
+  = do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
+       ; lintTyBndr tv $ \tv' ->
+          do { k <- lintType ty
+             ; lintL (not (tv' `elemVarSet` tyCoVarsOfType k))
+                     (text "Variable escape in forall:" <+> ppr t)
+             ; lintL (classifiesTypeWithValues k)
+                     (text "Non-* and non-# kind in forall:" <+> ppr t)
+             ; return k }}
 
 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
 
+lintType (CastTy ty co)
+  = do { k1 <- lintType ty
+       ; (k1', k2) <- lintStarCoercion co
+       ; ensureEqTys k1 k1' (mkCastErr ty co k1' k1)
+       ; return k2 }
+
+lintType (CoercionTy co)
+  = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
+       ; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 }
+
 lintKind :: OutKind -> LintM ()
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintKind k = do { sk <- lintType k
-                ; unless (isSuperKind sk)
-                         (addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
-                                      2 (ptext (sLit "has kind:") <+> ppr sk))) }
+                ; unless ((isStarKind sk) || (isUnliftedTypeKind sk))
+                         (addErrL (hang (text "Ill-kinded kind:" <+> ppr k)
+                                      2 (text "has kind:" <+> ppr sk))) }
+
+-- confirms that a type is really *
+lintStar :: SDoc -> OutKind -> LintM ()
+lintStar doc k
+  = lintL (classifiesTypeWithValues k)
+          (text "Non-*-like kind when *-like expected:" <+> ppr k $$
+           text "when checking" <+> doc)
 
 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintArrow what k1 k2   -- Eg lintArrow "type or kind `blah'" k1 k2
                        -- or lintarrow "coercion `blah'" k1 k2
-  | isSuperKind k1
-  = return superKind
-  | otherwise
-  = do { unless (okArrowArgKind k1)    (addErrL (msg (ptext (sLit "argument")) k1))
-       ; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result"))   k2))
+  = do { unless (okArrowArgKind k1)    (addErrL (msg (text "argument") k1))
+       ; unless (okArrowResultKind k2) (addErrL (msg (text "result")   k2))
        ; return liftedTypeKind }
   where
     msg ar k
-      = vcat [ hang (ptext (sLit "Ill-kinded") <+> ar)
-                  2 (ptext (sLit "in") <+> what)
-             , what <+> ptext (sLit "kind:") <+> ppr k ]
+      = vcat [ hang (text "Ill-kinded" <+> ar)
+                  2 (text "in" <+> what)
+             , what <+> text "kind:" <+> ppr k ]
 
 lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
 lint_ty_app ty k tys
-  = lint_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
+  = lint_app (text "type" <+> quotes (ppr ty)) k tys
 
 ----------------
 lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
 lint_co_app ty k tys
-  = lint_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys
+  = lint_app (text "coercion" <+> quotes (ppr ty)) k tys
 
 ----------------
 lintTyLit :: TyLit -> LintM ()
 lintTyLit (NumTyLit n)
   | n >= 0    = return ()
   | otherwise = failWithL msg
-    where msg = ptext (sLit "Negative type literal:") <+> integer n
+    where msg = text "Negative type literal:" <+> integer n
 lintTyLit (StrTyLit _) = return ()
 
 lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
@@ -1091,25 +1137,28 @@ lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lint_app doc kfn kas
-    = foldlM go_app kfn kas
+    = do { in_scope <- getInScope
+         -- We need the in_scope set to satisfy the invariant in
+         -- Note [The substitution invariant] in TyCoRep
+         ; foldlM (go_app in_scope) kfn kas }
   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 kas) ]
+    fail_msg = vcat [ hang (text "Kind application error in") 2 doc
+                    , nest 2 (text "Function kind =" <+> ppr kfn)
+                    , nest 2 (text "Arg kinds =" <+> ppr kas) ]
 
-    go_app kfn ka
+    go_app in_scope kfn ka
       | Just kfn' <- coreView kfn
-      = go_app kfn' ka
+      = go_app in_scope kfn' ka
 
-    go_app (FunTy kfa kfb) (_,ka)
-      = do { unless (ka `isSubKind` kfa) (addErrL fail_msg)
+    go_app _ (ForAllTy (Anon kfa) kfb) (_,ka)
+      = do { unless (ka `eqType` kfa) (addErrL fail_msg)
            ; return kfb }
 
-    go_app (ForAllTy kv kfn) (ta,ka)
-      = do { unless (ka `isSubKind` tyVarKind kv) (addErrL fail_msg)
-           ; return (substKiWith [kv] [ta] kfn) }
+    go_app in_scope (ForAllTy (Named kv _vis) kfn) (ta,ka)
+      = do { unless (ka `eqType` tyVarKind kv) (addErrL fail_msg)
+           ; return (substTyWithInScope in_scope [kv] [ta] kfn) }
 
-    go_app _ _ = failWithL fail_msg
+    go_app _ _ = failWithL fail_msg
 
 {- *********************************************************************
 *                                                                      *
@@ -1126,16 +1175,16 @@ lintCoreRule fun_ty (Rule { ru_name = name, ru_bndrs = bndrs
   = lintBinders bndrs $ \ _ ->
     do { lhs_ty <- foldM lintCoreArg fun_ty args
        ; rhs_ty <- lintCoreExpr rhs
-       ; checkTys lhs_ty rhs_ty $
-         (rule_doc <+> vcat [ ptext (sLit "lhs type:") <+> ppr lhs_ty
-                            , ptext (sLit "rhs type:") <+> ppr rhs_ty ])
+       ; ensureEqTys lhs_ty rhs_ty $
+         (rule_doc <+> vcat [ text "lhs type:" <+> ppr lhs_ty
+                            , text "rhs type:" <+> ppr rhs_ty ])
        ; let bad_bndrs = filterOut (`elemVarSet` exprsFreeVars args) bndrs
        ; checkL (null bad_bndrs)
-                (rule_doc <+> ptext (sLit "unbound") <+> ppr bad_bndrs)
+                (rule_doc <+> text "unbound" <+> ppr bad_bndrs)
             -- See Note [Linting rules]
     }
   where
-    rule_doc = ptext (sLit "Rule") <+> doubleQuotes (ftext name) <> colon
+    rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon
 
 {- Note [Linting rules]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -1162,7 +1211,7 @@ this check will nail it.
 ************************************************************************
 -}
 
-lintInCo :: InCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
+lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
 -- Check the coercion, and apply the substitution to it
 -- See Note [Linting type lets]
 lintInCo co
@@ -1170,79 +1219,114 @@ lintInCo co
     do  { co' <- applySubstCo co
         ; lintCoercion co' }
 
-lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
+-- lints a coercion, confirming that its lh kind and its rh kind are both *
+-- also ensures that the role is Nominal
+lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
+lintStarCoercion g
+  = do { (k1, k2, t1, t2, r) <- lintCoercion g
+       ; lintStar (text "the kind of the left type in" <+> ppr g) k1
+       ; lintStar (text "the kind of the right type in" <+> ppr g) k2
+       ; lintRole g Nominal r
+       ; return (t1, t2) }
+
+lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
 -- Check the kind of a coercion term, returning the kind
 -- Post-condition: the returned OutTypes are lint-free
---                 and have the same kind as each other
+--
+-- If   lintCorecion co = (k1, k2, s1, s2, r)
+-- then co :: s1 ~r s2
+--      s1 :: k2
+--      s2 :: k2
 
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintCoercion (Refl r ty)
   = do { k <- lintType ty
-       ; return (k, ty, ty, r) }
+       ; return (k, k, ty, ty, r) }
 
 lintCoercion co@(TyConAppCo r tc cos)
   | tc `hasKey` funTyConKey
   , [co1,co2] <- cos
-  = do { (k1,s1,t1,r1) <- lintCoercion co1
-       ; (k2,s2,t2,r2) <- lintCoercion co2
-       ; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
-       ; checkRole co1 r r1
-       ; checkRole co2 r r2
-       ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2, r) }
+  = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
+       ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
+       ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
+       ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
+       ; lintRole co1 r r1
+       ; lintRole co2 r r2
+       ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
 
   | Just {} <- synTyConDefn_maybe tc
-  = failWithL (ptext (sLit "Synonym in TyConAppCo:") <+> ppr co)
+  = failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
 
   | otherwise
-  = do { (ks,ss,ts,rs) <- mapAndUnzip4M lintCoercion cos
-       ; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
-       ; _ <- zipWith3M checkRole cos (tyConRolesX r tc) rs
-       ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts, r) }
+  = do { checkTyCon tc
+       ; (k's, ks, ss, ts, rs) <- mapAndUnzip5M lintCoercion cos
+       ; k' <- lint_co_app co (tyConKind tc) (ss `zip` k's)
+       ; k <- lint_co_app co (tyConKind tc) (ts `zip` ks)
+       ; _ <- zipWith3M lintRole cos (tyConRolesX r tc) rs
+       ; return (k', k, mkTyConApp tc ss, mkTyConApp tc ts, r) }
 
 lintCoercion co@(AppCo co1 co2)
-  = do { (k1,s1,t1,r1) <- lintCoercion co1
-       ; (k2,s2,t2,r2) <- lintCoercion co2
-       ; rk <- lint_co_app co k1 [(s2,k2)]
+  | TyConAppCo {} <- co1
+  = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co)
+  | Refl _ (TyConApp {}) <- co1
+  = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
+  | otherwise
+  = do { (k1,  k2,  s1, s2, r1) <- lintCoercion co1
+       ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2
+       ; k3 <- lint_co_app co k1 [(t1,k'1)]
+       ; k4 <- lint_co_app co k2 [(t2,k'2)]
        ; if r1 == Phantom
-         then checkL (r2 == Phantom || r2 == Nominal)
-                     (ptext (sLit "Second argument in AppCo cannot be R:") $$
+         then lintL (r2 == Phantom || r2 == Nominal)
+                     (text "Second argument in AppCo cannot be R:" $$
                       ppr co)
-         else checkRole co Nominal r2
-       ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2, r1) }
-
-lintCoercion (ForAllCo tv co)
-  = do { lintTyBndrKind tv
-       ; (k, s, t, r) <- addInScopeVar tv (lintCoercion co)
-       ; return (k, mkForAllTy tv s, mkForAllTy tv t, r) }
+         else lintRole co Nominal r2
+       ; return (k3, k4, mkAppTy s1 t1, mkAppTy s2 t2, r1) }
+
+----------
+lintCoercion (ForAllCo tv1 kind_co co)
+  = do { (_, k2) <- lintStarCoercion kind_co
+       ; let tv2 = setTyVarKind tv1 k2
+       ; (k3, k4, t1, t2, r) <- addInScopeVar tv1 $ lintCoercion co
+       ; let tyl = mkNamedForAllTy tv1 Invisible t1
+             tyr = mkNamedForAllTy tv2 Invisible $
+                   substTyWithUnchecked [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo kind_co] t2
+       ; return (k3, k4, tyl, tyr, r) }
 
 lintCoercion (CoVarCo cv)
   | not (isCoVar cv)
-  = failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
-                  2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
+  = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
+                  2 (text "With offending type:" <+> ppr (varType cv)))
   | otherwise
-  = do { checkTyCoVarInScope cv
+  = do { lintTyCoVarInScope cv
        ; cv' <- lookupIdInScope cv
-       ; let (s,t) = coVarKind cv'
-             k     = typeKind s
-             r     = coVarRole cv'
-       ; when (isSuperKind k) $
-         do { checkL (r == Nominal) (hang (ptext (sLit "Non-nominal kind equality"))
-                                     2 (ppr cv))
-            ; checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
-                                     2 (ppr cv)) }
-       ; return (k, s, t, r) }
+       ; lintUnliftedCoVar cv
+       ; return $ coVarKindsTypesRole cv' }
 
 -- See Note [Bad unsafe coercion]
-lintCoercion (UnivCo _prov r ty1 ty2)
+lintCoercion co@(UnivCo prov r ty1 ty2)
   = do { k1 <- lintType ty1
        ; k2 <- lintType ty2
---       ; unless (k1 `eqKind` k2) $
---         failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
---                       2 (ppr co))
-       ; when (r /= Phantom && isSubOpenTypeKind k1 && isSubOpenTypeKind k2)
+       ; case prov of
+           UnsafeCoerceProv -> return ()  -- no extra checks
+
+           PhantomProv kco    -> do { lintRole co Phantom r
+                                    ; check_kinds kco k1 k2 }
+
+           ProofIrrelProv kco -> do { lintL (isCoercionTy ty1) $
+                                          mkBadProofIrrelMsg ty1 co
+                                    ; lintL (isCoercionTy ty2) $
+                                          mkBadProofIrrelMsg ty2 co
+                                    ; check_kinds kco k1 k2 }
+
+           PluginProv _     -> return ()  -- no extra checks
+           HoleProv h       -> addErrL $
+                               text "Unfilled coercion hole:" <+> ppr h
+
+       ; when (r /= Phantom && classifiesTypeWithValues k1
+                            && classifiesTypeWithValues k2)
               (checkTypes ty1 ty2)
-       ; return (k1, ty1, ty2, r) }
+       ; return (k1, k2, ty1, ty2, r) }
    where
      report s = hang (text $ "Unsafe coercion between " ++ s)
                      2 (vcat [ text "From:" <+> ppr ty1
@@ -1276,149 +1360,170 @@ lintCoercion (UnivCo _prov r ty1 ty2)
                 _          -> return ()
             }
 
+     check_kinds kco k1 k2 = do { (k1', k2') <- lintStarCoercion kco
+                                ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft  co)
+                                ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
+
+
 lintCoercion (SymCo co)
-  = do { (k, ty1, ty2, r) <- lintCoercion co
-       ; return (k, ty2, ty1, r) }
+  = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
+       ; return (k2, k1, ty2, ty1, r) }
 
 lintCoercion co@(TransCo co1 co2)
-  = do { (k1, ty1a, ty1b, r1) <- lintCoercion co1
-       ; (_ ty2a, ty2b, r2) <- 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]))
-       ; checkRole co r1 r2
-       ; return (k1, ty1a, ty2b, r1) }
+  = do { (k1a, _k1b, ty1a, ty1b, r1) <- lintCoercion co1
+       ; (_k2a, k2b, ty2a, ty2b, r2) <- lintCoercion co2
+       ; ensureEqTys ty1b ty2a
+               (hang (text "Trans coercion mis-match:" <+> ppr co)
+                   2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
+       ; lintRole co r1 r2
+       ; return (k1a, k2b, ty1a, ty2b, r1) }
 
 lintCoercion the_co@(NthCo n co)
-  = do { (_,s,t,r) <- lintCoercion co
-       ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
-           (Just (tc_s, tys_s), Just (tc_t, tys_t))
+  = do { (_, _, s, t, r) <- lintCoercion co
+       ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
+         { (Just (tv_s, _ty_s), Just (tv_t, _ty_t))
+             |  n == 0
+             -> return (ks, kt, ts, tt, Nominal)
+             where
+               ts = tyVarKind tv_s
+               tt = tyVarKind tv_t
+               ks = typeKind ts
+               kt = typeKind tt
+
+         ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
+         { (Just (tc_s, tys_s), Just (tc_t, tys_t))
              | tc_s == tc_t
              , isInjectiveTyCon tc_s r
-                 -- see Note [NthCo and newtypes] in Coercion
+                 -- see Note [NthCo and newtypes] in TyCoRep
              , tys_s `equalLength` tys_t
              , n < length tys_s
-             -> return (ks, ts, tt, tr)
+             -> return (ks, kt, ts, tt, tr)
              where
                ts = getNth tys_s n
                tt = getNth tys_t n
                tr = nthRole r tc_s n
                ks = typeKind ts
+               kt = typeKind tt
 
-           _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
-                              2 (ppr the_co $$ ppr s $$ ppr t)) }
+         ; _ -> failWithL (hang (text "Bad getNth:")
+                              2 (ppr the_co $$ ppr s $$ ppr t)) }}}
 
 lintCoercion the_co@(LRCo lr co)
-  = do { (_,s,t,r) <- lintCoercion co
-       ; checkRole co Nominal r
+  = do { (_,_,s,t,r) <- lintCoercion co
+       ; lintRole co Nominal r
        ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
            (Just s_pr, Just t_pr)
-             -> return (k, s_pick, t_pick, Nominal)
+             -> return (ks_pick, kt_pick, s_pick, t_pick, Nominal)
              where
-               s_pick = pickLR lr s_pr
-               t_pick = pickLR lr t_pr
-               k = typeKind s_pick
+               s_pick  = pickLR lr s_pr
+               t_pick  = pickLR lr t_pr
+               ks_pick = typeKind s_pick
+               kt_pick = typeKind t_pick
 
-           _ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
+           _ -> failWithL (hang (text "Bad LRCo:")
                               2 (ppr the_co $$ ppr s $$ ppr t)) }
 
-lintCoercion (InstCo co arg_ty)
-  = do { (k,s,t,r) <- lintCoercion co
-       ; arg_kind  <- lintType arg_ty
-       ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
-          (Just (tv1,ty1), Just (tv2,ty2))
-            | arg_kind `isSubKind` tyVarKind tv1
-            -> return (k, substTyWith [tv1] [arg_ty] ty1,
-                          substTyWith [tv2] [arg_ty] ty2, r)
+lintCoercion (InstCo co arg)
+  = do { (k3, k4, t1',t2', r) <- lintCoercion co
+       ; (k1',k2',s1,s2, r') <- lintCoercion arg
+       ; lintRole arg Nominal r'
+       ; case (splitForAllTy_maybe t1', splitForAllTy_maybe t2') of
+          (Just (tv1,t1), Just (tv2,t2))
+            | k1' `eqType` tyVarKind tv1
+            , k2' `eqType` tyVarKind tv2
+            -> return (k3, k4,
+                       substTyWith [tv1] [s1] t1,
+                       substTyWith [tv2] [s2] t2, r)
             | otherwise
-            -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
-          _ -> failWithL (ptext (sLit "Bad argument of inst")) }
+            -> failWithL (text "Kind mis-match in inst coercion")
+          _ -> failWithL (text "Bad argument of inst") }
 
 lintCoercion co@(AxiomInstCo con ind cos)
-  = do { unless (0 <= ind && ind < brListLength (coAxiomBranches con))
-                (bad_ax (ptext (sLit "index out of range")))
-         -- See Note [Kind instantiation in coercions]
+  = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
+                (bad_ax (text "index out of range"))
        ; let CoAxBranch { cab_tvs   = ktvs
+                        , cab_cvs   = cvs
                         , cab_roles = roles
                         , cab_lhs   = lhs
                         , cab_rhs   = rhs } = coAxiomNthBranch con ind
-       ; unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths")))
-       ; in_scope <- getInScope
-       ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
+       ; unless (length ktvs + length cvs == length cos) $
+           bad_ax (text "lengths")
+       ; subst <- getTCvSubst
+       ; let empty_subst = zapTCvSubst subst
        ; (subst_l, subst_r) <- foldlM check_ki
                                       (empty_subst, empty_subst)
-                                      (zip3 ktvs roles cos)
-       ; let lhs' = Type.substTys subst_l lhs
-             rhs' = Type.substTy subst_r rhs
+                                      (zip3 (ktvs ++ cvs) roles cos)
+       ; let lhs' = substTys subst_l lhs
+             rhs' = substTy  subst_r rhs
        ; case checkAxInstCo co of
-           Just bad_branch -> bad_ax $ ptext (sLit "inconsistent with") <+> (pprCoAxBranch (coAxiomTyCon con) bad_branch)
+           Just bad_branch -> bad_ax $ text "inconsistent with" <+>
+                                       pprCoAxBranch con bad_branch
            Nothing -> return ()
-       ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs', coAxiomRole con) }
+       ; let s2 = mkTyConApp (coAxiomTyCon con) lhs'
+       ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) }
   where
-    bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
+    bad_ax what = addErrL (hang (text  "Bad axiom application" <+> parens what)
                         2 (ppr co))
 
-    check_ki (subst_l, subst_r) (ktv, role, co)
-      = do { (k, t1, t2, r) <- lintCoercion co
-           ; checkRole co role r
-           ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
-                  -- Using subst_l is ok, because subst_l and subst_r
-                  -- must agree on kind equalities
-           ; unless (k `isSubKind` ktv_kind)
-                    (bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
-           ; return (Type.extendTvSubst subst_l ktv t1,
-                     Type.extendTvSubst subst_r ktv t2) }
-
-lintCoercion co@(SubCo co')
-  = do { (k,s,t,r) <- lintCoercion co'
-       ; checkRole co Nominal r
-       ; return (k,s,t,Representational) }
-
-
-lintCoercion this@(AxiomRuleCo co ts cs)
-  = do _ks <- mapM lintType ts
-       eqs <- mapM lintCoercion cs
-
-       let tyNum = length ts
-
-       case compare (coaxrTypeArity co) tyNum of
-         EQ -> return ()
-         LT -> err "Too many type arguments"
-                    [ txt "expected" <+> int (coaxrTypeArity co)
-                    , txt "provided" <+> int tyNum ]
-         GT -> err "Not enough type arguments"
-                    [ txt "expected" <+> int (coaxrTypeArity co)
-                          , txt "provided" <+> int tyNum ]
-       checkRoles 0 (coaxrAsmpRoles co) eqs
-
-       case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
-         Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
-         Just (Pair l r) ->
-           do kL <- lintType l
-              kR <- lintType r
-              unless (eqKind kL kR)
-                $ err "Kind error in CoAxiomRule"
-                       [ppr kL <+> txt "/=" <+> ppr kR]
-              return (kL, l, r, coaxrRole co)
+    check_ki (subst_l, subst_r) (ktv, role, arg)
+      = do { (k', k'', s', t', r) <- lintCoercion arg
+           ; lintRole arg role r
+           ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
+                 ktv_kind_r = substTy subst_r (tyVarKind ktv)
+           ; unless (k' `eqType` ktv_kind_l)
+                    (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr k', ppr ktv, ppr ktv_kind_l ] ))
+           ; unless (k'' `eqType` ktv_kind_r)
+                    (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr k'', ppr ktv, ppr ktv_kind_r ] ))
+           ; return (extendTCvSubst subst_l ktv s',
+                     extendTCvSubst subst_r ktv t') }
+
+lintCoercion (CoherenceCo co1 co2)
+  = do { (_, k2, t1, t2, r) <- lintCoercion co1
+       ; let lhsty = mkCastTy t1 co2
+       ; k1' <- lintType lhsty
+       ; return (k1', k2, lhsty, t2, r) }
+
+lintCoercion (KindCo co)
+  = do { (k1, k2, _, _, _) <- lintCoercion co
+       ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
+
+lintCoercion (SubCo co')
+  = do { (k1,k2,s,t,r) <- lintCoercion co'
+       ; lintRole co' Nominal r
+       ; return (k1,k2,s,t,Representational) }
+
+lintCoercion this@(AxiomRuleCo co cs)
+  = do { eqs <- mapM lintCoercion cs
+       ; lintRoles 0 (coaxrAsmpRoles co) eqs
+       ; case coaxrProves co [ Pair l r | (_,_,l,r,_) <- eqs ] of
+           Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
+           Just (Pair l r) ->
+             return (typeKind l, typeKind r, l, r, coaxrRole co) }
   where
-  txt       = ptext . sLit
   err m xs  = failWithL $
-                hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
+                hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName co) : xs)
 
-  checkRoles n (e : es) ((_,_,_,r) : rs)
-    | e == r    = checkRoles (n+1) es rs
+  lintRoles n (e : es) ((_,_,_,_,r) : rs)
+    | e == r    = lintRoles (n+1) es rs
     | otherwise = err "Argument roles mismatch"
-                      [ txt "In argument:" <+> int (n+1)
-                      , txt "Expected:" <+> ppr e
-                      , txt "Found:" <+> ppr r ]
-  checkRoles _ [] []  = return ()
-  checkRoles n [] rs  = err "Too many coercion arguments"
-                          [ txt "Expected:" <+> int n
-                          , txt "Provided:" <+> int (n + length rs) ]
-
-  checkRoles n es []  = err "Not enough coercion arguments"
-                          [ txt "Expected:" <+> int (n + length es)
-                          , txt "Provided:" <+> int n ]
+                      [ text "In argument:" <+> int (n+1)
+                      , text "Expected:" <+> ppr e
+                      , text "Found:" <+> ppr r ]
+  lintRoles _ [] []  = return ()
+  lintRoles n [] rs  = err "Too many coercion arguments"
+                          [ text "Expected:" <+> int n
+                          , text "Provided:" <+> int (n + length rs) ]
+
+  lintRoles n es []  = err "Not enough coercion arguments"
+                          [ text "Expected:" <+> int (n + length es)
+                          , text "Provided:" <+> int n ]
+
+----------
+lintUnliftedCoVar :: CoVar -> LintM ()
+lintUnliftedCoVar cv
+  = when (not (isUnliftedType (coVarKind cv))) $
+    failWithL (text "Bad lifted equality:" <+> ppr cv
+                 <+> dcolon <+> ppr (coVarKind cv))
 
 {-
 ************************************************************************
@@ -1433,7 +1538,7 @@ lintCoercion this@(AxiomRuleCo co ts cs)
 data LintEnv
   = LE { le_flags :: LintFlags       -- Linting the result of this pass
        , le_loc   :: [LintLocInfo]   -- Locations
-       , le_subst :: TvSubst         -- Current type substitution; we also use this
+       , le_subst :: TCvSubst        -- Current type substitution; we also use this
                                      -- to keep track of all the variables in scope,
                                      -- both Ids and TyVars
        , le_dynflags :: DynFlags     -- DynamicFlags
@@ -1480,11 +1585,10 @@ instance Functor LintM where
       fmap = liftM
 
 instance Applicative LintM where
-      pure = return
+      pure x = LintM $ \ _ errs -> (Just x, errs)
       (<*>) = ap
 
 instance Monad LintM where
-  return x = LintM (\ _ errs -> (Just x, errs))
   fail err = failWithL (text err)
   m >>= k  = LintM (\ env errs ->
                        let (res, errs') = unLintM m env errs in
@@ -1492,6 +1596,11 @@ instance Monad LintM where
                            Just r -> unLintM (k r) env errs'
                            Nothing -> (Nothing, errs'))
 
+#if __GLASGOW_HASKELL__ > 710
+instance MonadFail.MonadFail LintM where
+    fail err = failWithL (text err)
+#endif
+
 instance HasDynFlags LintM where
   getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
 
@@ -1512,7 +1621,7 @@ initL dflags flags m
   = case unLintM m env (emptyBag, emptyBag) of
       (_, errs) -> errs
   where
-    env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [], le_dynflags = dflags }
+    env = LE { le_flags = flags, le_subst = emptyTCvSubst, le_loc = [], le_dynflags = dflags }
 
 getLintFlags :: LintM LintFlags
 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
@@ -1521,6 +1630,10 @@ checkL :: Bool -> MsgDoc -> LintM ()
 checkL True  _   = return ()
 checkL False msg = failWithL msg
 
+-- like checkL, but relevant to type checking
+lintL :: Bool -> MsgDoc -> LintM ()
+lintL = checkL
+
 checkWarnL :: Bool -> MsgDoc -> LintM ()
 checkWarnL True   _  = return ()
 checkWarnL False msg = addWarnL msg
@@ -1546,7 +1659,7 @@ addMsg env msgs msg
    (loc, cxt1) = dumpLoc (head locs)
    cxts        = [snd (dumpLoc loc) | loc <- locs]
    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
-                                      ptext (sLit "Substitution:") <+> ppr (le_subst env)
+                                      text "Substitution:" <+> ppr (le_subst env)
                | otherwise          = cxt1
 
    mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
@@ -1565,76 +1678,77 @@ inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
 addInScopeVars :: [Var] -> LintM a -> LintM a
 addInScopeVars vars m
   = LintM $ \ env errs ->
-    unLintM m (env { le_subst = extendTvInScopeList (le_subst env) vars })
+    unLintM m (env { le_subst = extendTCvInScopeList (le_subst env) vars })
               errs
 
 addInScopeVar :: Var -> LintM a -> LintM a
 addInScopeVar var m
   = LintM $ \ env errs ->
-    unLintM m (env { le_subst = extendTvInScope (le_subst env) var }) errs
+    unLintM m (env { le_subst = extendTCvInScope (le_subst env) var }) errs
 
 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
 extendSubstL tv ty m
   = LintM $ \ env errs ->
     unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
 
-updateTvSubst :: TvSubst -> LintM a -> LintM a
-updateTvSubst subst' m
+updateTCvSubst :: TCvSubst -> LintM a -> LintM a
+updateTCvSubst subst' m
   = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
 
-getTvSubst :: LintM TvSubst
-getTvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
+getTCvSubst :: LintM TCvSubst
+getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
 
 getInScope :: LintM InScopeSet
-getInScope = LintM (\ env errs -> (Just (getTvInScope (le_subst env)), errs))
+getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs))
 
 applySubstTy :: InType -> LintM OutType
-applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
+applySubstTy ty = do { subst <- getTCvSubst; return (substTy subst ty) }
 
 applySubstCo :: InCoercion -> LintM OutCoercion
-applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
+applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
 
 lookupIdInScope :: Id -> LintM Id
 lookupIdInScope id
   | not (mustHaveLocalBinding id)
   = return id   -- An imported Id
   | otherwise
-  = do  { subst <- getTvSubst
-        ; case lookupInScope (getTvInScope subst) id of
+  = do  { subst <- getTCvSubst
+        ; case lookupInScope (getTCvInScope subst) id of
                 Just v  -> return v
                 Nothing -> do { addErrL out_of_scope
                               ; return id } }
   where
-    out_of_scope = pprBndr LetBind id <+> ptext (sLit "is out of scope")
+    out_of_scope = pprBndr LetBind id <+> text "is out of scope"
 
 
 oneTupleDataConId :: Id -- Should not happen
 oneTupleDataConId = dataConWorkId (tupleDataCon Boxed 1)
 
-checkTyCoVarInScope :: Var -> LintM ()
-checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
+lintTyCoVarInScope :: Var -> LintM ()
+lintTyCoVarInScope v = lintInScope (text "is out of scope") v
 
-checkInScope :: SDoc -> Var -> LintM ()
-checkInScope loc_msg var =
- do { subst <- getTvSubst
-    ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
+lintInScope :: SDoc -> Var -> LintM ()
+lintInScope loc_msg var =
+ do { subst <- getTCvSubst
+    ; lintL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
              (hsep [pprBndr LetBind var, loc_msg]) }
 
-checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
+ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
 -- check ty2 is subtype of ty1 (ie, has same structure but usage
 -- annotations need only be consistent, not equal)
 -- Assumes ty1,ty2 are have alrady had the substitution applied
-checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
+ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg
 
-checkRole :: Coercion
+lintRole :: Outputable thing
+          => thing     -- where the role appeared
           -> Role      -- expected
           -> Role      -- actual
           -> LintM ()
-checkRole co r1 r2
-  = checkL (r1 == r2)
-           (ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+>
-            ptext (sLit "got") <+> ppr r2 $$
-            ptext (sLit "in") <+> ppr co)
+lintRole co r1 r2
+  = lintL (r1 == r2)
+          (text "Role incompatibility: expected" <+> ppr r1 <> comma <+>
+           text "got" <+> ppr r2 $$
+           text "in" <+> ppr co)
 
 {-
 ************************************************************************
@@ -1647,16 +1761,16 @@ checkRole co r1 r2
 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
 
 dumpLoc (RhsOf v)
-  = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
+  = (getSrcLoc v, brackets (text "RHS of" <+> pp_binders [v]))
 
 dumpLoc (LambdaBodyOf b)
-  = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
+  = (getSrcLoc b, brackets (text "in body of lambda with binder" <+> pp_binder b))
 
 dumpLoc (BodyOfLetRec [])
-  = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
+  = (noSrcLoc, brackets (text "In body of a letrec with no binders"))
 
 dumpLoc (BodyOfLetRec bs@(_:_))
-  = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
+  = ( getSrcLoc (head bs), brackets (text "in body of letrec with binders" <+> pp_binders bs))
 
 dumpLoc (AnExpr e)
   = (noSrcLoc, text "In the expression:" <+> ppr e)
@@ -1668,7 +1782,7 @@ dumpLoc (CasePat (con, args, _))
   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
 
 dumpLoc (ImportedUnfolding locn)
-  = (locn, brackets (ptext (sLit "in an imported unfolding")))
+  = (locn, brackets (text "in an imported unfolding"))
 dumpLoc TopLevelBindings
   = (noSrcLoc, Outputable.empty)
 dumpLoc (InType ty)
@@ -1696,12 +1810,12 @@ mkCaseAltMsg e ty1 ty2
   = hang (text "Type of case alternatives not the same as the annotation on case:")
          4 (vcat [ppr ty1, ppr ty2, ppr e])
 
-mkScrutMsg :: Id -> Type -> Type -> TvSubst -> MsgDoc
+mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> MsgDoc
 mkScrutMsg var var_ty scrut_ty subst
   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
           text "Result binder type:" <+> ppr var_ty,--(idType var),
           text "Scrutinee type:" <+> ppr scrut_ty,
-     hsep [ptext (sLit "Current TV subst"), ppr subst]]
+     hsep [text "Current TCv subst", ppr subst]]
 
 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
 mkNonDefltMsg e
@@ -1751,108 +1865,128 @@ mkNewTyDataConAltMsg scrut_ty alt
 
 mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
 mkAppMsg fun_ty arg_ty arg
-  = vcat [ptext (sLit "Argument value doesn't match argument type:"),
-              hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
-              hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
-              hang (ptext (sLit "Arg:")) 4 (ppr arg)]
+  = vcat [text "Argument value doesn't match argument type:",
+              hang (text "Fun type:") 4 (ppr fun_ty),
+              hang (text "Arg type:") 4 (ppr arg_ty),
+              hang (text "Arg:") 4 (ppr arg)]
 
 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
 mkNonFunAppMsg fun_ty arg_ty arg
-  = vcat [ptext (sLit "Non-function type in function position"),
-              hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
-              hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
-              hang (ptext (sLit "Arg:")) 4 (ppr arg)]
+  = vcat [text "Non-function type in function position",
+              hang (text "Fun type:") 4 (ppr fun_ty),
+              hang (text "Arg type:") 4 (ppr arg_ty),
+              hang (text "Arg:") 4 (ppr arg)]
 
 mkLetErr :: TyVar -> CoreExpr -> MsgDoc
 mkLetErr bndr rhs
-  = vcat [ptext (sLit "Bad `let' binding:"),
-          hang (ptext (sLit "Variable:"))
+  = vcat [text "Bad `let' binding:",
+          hang (text "Variable:")
                  4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
-          hang (ptext (sLit "Rhs:"))
+          hang (text "Rhs:")
                  4 (ppr rhs)]
 
 mkTyAppMsg :: Type -> Type -> MsgDoc
 mkTyAppMsg ty arg_ty
   = vcat [text "Illegal type application:",
-              hang (ptext (sLit "Exp type:"))
+              hang (text "Exp type:")
                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
-              hang (ptext (sLit "Arg type:"))
+              hang (text "Arg type:")
                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 
 mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
 mkRhsMsg binder what ty
   = vcat
-    [hsep [ptext (sLit "The type of this binder doesn't match the type of its") <+> what <> colon,
+    [hsep [text "The type of this binder doesn't match the type of its" <+> what <> colon,
             ppr binder],
-     hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
-     hsep [ptext (sLit "Rhs type:"), ppr ty]]
+     hsep [text "Binder's type:", ppr (idType binder)],
+     hsep [text "Rhs type:", ppr ty]]
 
 mkLetAppMsg :: CoreExpr -> MsgDoc
 mkLetAppMsg e
-  = hang (ptext (sLit "This argument does not satisfy the let/app invariant:"))
+  = hang (text "This argument does not satisfy the let/app invariant:")
        2 (ppr e)
 
 mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
 mkRhsPrimMsg binder _rhs
-  = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
+  = vcat [hsep [text "The type of this binder is primitive:",
                      ppr binder],
-              hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
+              hsep [text "Binder's type:", ppr (idType binder)]
              ]
 
 mkStrictMsg :: Id -> MsgDoc
 mkStrictMsg binder
-  = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
+  = vcat [hsep [text "Recursive or top-level binder has strict demand info:",
                      ppr binder],
-              hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
+              hsep [text "Binder's demand info:", ppr (idDemandInfo binder)]
              ]
 
 mkNonTopExportedMsg :: Id -> MsgDoc
 mkNonTopExportedMsg binder
-  = hsep [ptext (sLit "Non-top-level binder is marked as exported:"), ppr binder]
+  = hsep [text "Non-top-level binder is marked as exported:", ppr binder]
 
 mkNonTopExternalNameMsg :: Id -> MsgDoc
 mkNonTopExternalNameMsg binder
-  = hsep [ptext (sLit "Non-top-level binder has an external name:"), ppr binder]
+  = hsep [text "Non-top-level binder has an external name:", ppr binder]
 
 mkKindErrMsg :: TyVar -> Type -> MsgDoc
 mkKindErrMsg tyvar arg_ty
-  = vcat [ptext (sLit "Kinds don't match in type application:"),
-          hang (ptext (sLit "Type variable:"))
+  = vcat [text "Kinds don't match in type application:",
+          hang (text "Type variable:")
                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
-          hang (ptext (sLit "Arg type:"))
+          hang (text "Arg type:")
                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 
 {- Not needed now
 mkArityMsg :: Id -> MsgDoc
 mkArityMsg binder
-  = vcat [hsep [ptext (sLit "Demand type has"),
+  = vcat [hsep [text "Demand type has",
                 ppr (dmdTypeDepth dmd_ty),
-                ptext (sLit "arguments, rhs has"),
+                text "arguments, rhs has",
                 ppr (idArity binder),
-                ptext (sLit "arguments,"),
+                text "arguments,",
                 ppr binder],
-              hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
+              hsep [text "Binder's strictness signature:", ppr dmd_ty]
 
          ]
            where (StrictSig dmd_ty) = idStrictness binder
 -}
-mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
+mkCastErr :: Outputable casted => casted -> Coercion -> Type -> Type -> MsgDoc
 mkCastErr expr co from_ty expr_ty
-  = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
-          ptext (sLit "From-type:") <+> ppr from_ty,
-          ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty,
-          ptext (sLit "Actual enclosed expr:") <+> ppr expr,
-          ptext (sLit "Coercion used in cast:") <+> ppr co
+  = vcat [text "From-type of Cast differs from type of enclosed expression",
+          text "From-type:" <+> ppr from_ty,
+          text "Type of enclosed expr:" <+> ppr expr_ty,
+          text "Actual enclosed expr:" <+> ppr expr,
+          text "Coercion used in cast:" <+> ppr co
          ]
 
+mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
+mkBadUnivCoMsg lr co
+  = text "Kind mismatch on the" <+> pprLeftOrRight lr <+>
+    text "side of a UnivCo:" <+> ppr co
+
+mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
+mkBadProofIrrelMsg ty co
+  = hang (text "Found a non-coercion in a proof-irrelevance UnivCo:")
+       2 (vcat [ text "type:" <+> ppr ty
+               , text "co:" <+> ppr co ])
+
+mkBadTyVarMsg :: Var -> SDoc
+mkBadTyVarMsg tv
+  = text "Non-tyvar used in TyVarTy:"
+      <+> ppr tv <+> dcolon <+> ppr (varType tv)
+
+pprLeftOrRight :: LeftOrRight -> MsgDoc
+pprLeftOrRight CLeft  = text "left"
+pprLeftOrRight CRight = text "right"
+
 dupVars :: [[Var]] -> MsgDoc
 dupVars vars
-  = hang (ptext (sLit "Duplicate variables brought into scope"))
+  = hang (text "Duplicate variables brought into scope")
        2 (ppr vars)
 
 dupExtVars :: [[Name]] -> MsgDoc
 dupExtVars vars
-  = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
+  = hang (text "Duplicate top-level variables with the same qualified name")
        2 (ppr vars)
 
 {-
@@ -1893,21 +2027,22 @@ lintAnnots pname pass guts = do
   return nguts
 
 -- | Run the given pass without annotations. This means that we both
--- remove the @Opt_Debug@ flag from the environment as well as all
+-- set the debugLevel setting to 0 in the environment as well as all
 -- annotations from incoming modules.
 withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
 withoutAnnots pass guts = do
   -- Remove debug flag from environment.
   dflags <- getDynFlags
-  let removeFlag env = env{hsc_dflags = gopt_unset dflags Opt_Debug}
+  let removeFlag env = env{ hsc_dflags = dflags{ debugLevel = 0} }
       withoutFlag corem =
         liftIO =<< runCoreM <$> fmap removeFlag getHscEnv <*> getRuleBase <*>
                                 getUniqueSupplyM <*> getModule <*>
                                 getVisibleOrphanMods <*>
-                                getPrintUnqualified <*> pure corem
+                                getPrintUnqualified <*> getSrcSpanM <*>
+                                pure corem
   -- Nuke existing ticks in module.
   -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
-  -- them in absence of @Opt_Debug@?
+  -- them in absence of debugLevel > 0.
   let nukeTicks = stripTicksE (not . tickishIsCode)
       nukeAnnotsBind :: CoreBind -> CoreBind
       nukeAnnotsBind bind = case bind of