Remove decideKindGeneralisationPlan

TypeInType came with a new function: decideKindGeneralisationPlan.
This type-level counterpart to the term-level decideGeneralisationPlan
chose whether or not a kind should be generalized. The thinking was
that if `let` should not be generalized, then kinds shouldn't either
(under the same circumstances around -XMonoLocalBinds).

However, this is too conservative -- the situation described in the
motivation for "let should be be generalized" does not occur in types.

This commit thus removes decideKindGeneralisationPlan, always
generalizing.

One consequence is that tc_hs_sig_type_and_gen no longer calls
solveEqualities, which reports all unsolved constraints, instead
relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect
of this is that reporing kind errors gets delayed more frequently.
This seems to be a net benefit in error reporting; often, alongside
a kind error, the type error is now reported (and users might find
type errors easier to understand).

Some of these errors ended up at the top level, where it was
discovered that the GlobalRdrEnv containing the definitions in the
local module was not in the TcGblEnv, and thus errors were reported
with qualified names unnecessarily. This commit rejiggers some of
the logic around captureTopConstraints accordingly.

One error message (typecheck/should_fail/T1633)
is a regression, mentioning the name of a default method. However,
that problem is already reported as #10087, its solution is far from
clear, and so I'm not addressing it here.

This commit fixes #15141. As it's an internal refactor, there is
no concrete test case for it.

Along the way, we no longer need the hsib_closed field of
HsImplicitBndrs (it was used only in decideKindGeneralisationPlan)
and so it's been removed, simplifying the datatype structure.

Along the way, I removed code in the validity checker that looks
at coercions. This isn't related to this patch, really (though
it was, at one point), but it's an improvement, so I kept it.

This updates the haddock submodule.

62 files changed, 621 insertions, 415 deletions

diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index bb3c46ba47..5b74487c5d 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -204,7 +204,7 @@ get_scoped_tvs (L _ signature)
       -- Both implicit and explicit quantified variables
       -- We need the implicit ones for   f :: forall (a::k). blah
       --    here 'k' scopes too
-      | HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_vars }
+      | HsIB { hsib_ext = implicit_vars
              , hsib_body = hs_ty } <- sig
       , (explicit_vars, _) <- splitLHsForAllTy hs_ty
       = implicit_vars ++ map hsLTyVarName explicit_vars
@@ -544,7 +544,7 @@ repTyFamInstD decl@(TyFamInstDecl { tfid_eqn = eqn })
        ; repTySynInst tc eqn1 }
 
 repTyFamEqn :: TyFamInstEqn GhcRn -> DsM (Core TH.TySynEqnQ)
-repTyFamEqn (HsIB { hsib_ext = HsIBRn { hsib_vars = var_names }
+repTyFamEqn (HsIB { hsib_ext = var_names
                   , hsib_body = FamEqn { feqn_pats = tys
                                        , feqn_rhs  = rhs }})
   = do { let hs_tvs = HsQTvs { hsq_ext = HsQTvsRn
@@ -561,7 +561,7 @@ repTyFamEqn (HsIB _ (XFamEqn _)) = panic "repTyFamEqn"
 
 repDataFamInstD :: DataFamInstDecl GhcRn -> DsM (Core TH.DecQ)
 repDataFamInstD (DataFamInstDecl { dfid_eqn =
-                  (HsIB { hsib_ext = HsIBRn { hsib_vars = var_names }
+                  (HsIB { hsib_ext = var_names
                         , hsib_body = FamEqn { feqn_tycon = tc_name
                                              , feqn_pats  = tys
                                              , feqn_rhs   = defn }})})
@@ -651,7 +651,7 @@ repRuleD (L _ (XRuleDecl _)) = panic "repRuleD"
 ruleBndrNames :: LRuleBndr GhcRn -> [Name]
 ruleBndrNames (L _ (RuleBndr _ n))      = [unLoc n]
 ruleBndrNames (L _ (RuleBndrSig _ n sig))
-  | HsWC { hswc_body = HsIB { hsib_ext = HsIBRn { hsib_vars = vars } }} <- sig
+  | HsWC { hswc_body = HsIB { hsib_ext = vars }} <- sig
   = unLoc n : vars
 ruleBndrNames (L _ (RuleBndrSig _ _ (HsWC _ (XHsImplicitBndrs _))))
   = panic "ruleBndrNames"
@@ -1042,7 +1042,7 @@ repContext ctxt = do preds <- repList typeQTyConName repLTy ctxt
                      repCtxt preds
 
 repHsSigType :: LHsSigType GhcRn -> DsM (Core TH.TypeQ)
-repHsSigType (HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_tvs }
+repHsSigType (HsIB { hsib_ext = implicit_tvs
                    , hsib_body = body })
   | (explicit_tvs, ctxt, ty) <- splitLHsSigmaTy body
   = addSimpleTyVarBinds implicit_tvs $
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index 8c5387ddb2..3939f57adb 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -20,7 +20,7 @@ module HsTypes (
         HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind,
         HsTyVarBndr(..), LHsTyVarBndr,
         LHsQTyVars(..), HsQTvsRn(..),
-        HsImplicitBndrs(..), HsIBRn(..),
+        HsImplicitBndrs(..),
         HsWildCardBndrs(..),
         LHsSigType, LHsSigWcType, LHsWcType,
         HsTupleSort(..),
@@ -332,23 +332,18 @@ isEmptyLHsQTvs _                = False
 
 -- | Haskell Implicit Binders
 data HsImplicitBndrs pass thing   -- See Note [HsType binders]
-  = HsIB { hsib_ext  :: XHsIB pass thing
+  = HsIB { hsib_ext  :: XHsIB pass thing -- after renamer: [Name]
+                                         -- Implicitly-bound kind & type vars
+                                         -- Order is important; see
+                                         -- Note [Ordering of implicit variables]
+
          , hsib_body :: thing            -- Main payload (type or list of types)
     }
   | XHsImplicitBndrs (XXHsImplicitBndrs pass thing)
 
-data HsIBRn
-  = HsIBRn { hsib_vars :: [Name] -- Implicitly-bound kind & type vars
-                                 -- Order is important; see
-                                 -- Note [Ordering of implicit variables]
-           , hsib_closed :: Bool -- Taking the hsib_vars into account,
-                                 -- is the payload closed? Used in
-                                 -- TcHsType.decideKindGeneralisationPlan
-    } deriving Data
-
 type instance XHsIB              GhcPs _ = NoExt
-type instance XHsIB              GhcRn _ = HsIBRn
-type instance XHsIB              GhcTc _ = HsIBRn
+type instance XHsIB              GhcRn _ = [Name]
+type instance XHsIB              GhcTc _ = [Name]
 
 type instance XXHsImplicitBndrs  (GhcPass _) _ = NoExt
 
@@ -429,9 +424,7 @@ mkHsWildCardBndrs x = HsWC { hswc_body = x
 -- Add empty binders.  This is a bit suspicious; what if
 -- the wrapped thing had free type variables?
 mkEmptyImplicitBndrs :: thing -> HsImplicitBndrs GhcRn thing
-mkEmptyImplicitBndrs x = HsIB { hsib_ext = HsIBRn
-                                  { hsib_vars   = []
-                                  , hsib_closed = False }
+mkEmptyImplicitBndrs x = HsIB { hsib_ext = []
                               , hsib_body = x }
 
 mkEmptyWildCardBndrs :: thing -> HsWildCardBndrs GhcRn thing
@@ -928,7 +921,7 @@ hsWcScopedTvs :: LHsSigWcType GhcRn -> [Name]
 -- because they scope in the same way
 hsWcScopedTvs sig_ty
   | HsWC { hswc_ext = nwcs, hswc_body = sig_ty1 }  <- sig_ty
-  , HsIB { hsib_ext = HsIBRn { hsib_vars = vars}
+  , HsIB { hsib_ext = vars
          , hsib_body = sig_ty2 } <- sig_ty1
   = case sig_ty2 of
       L _ (HsForAllTy { hst_bndrs = tvs }) -> vars ++ nwcs ++
@@ -942,7 +935,7 @@ hsWcScopedTvs (XHsWildCardBndrs _) = panic "hsWcScopedTvs"
 hsScopedTvs :: LHsSigType GhcRn -> [Name]
 -- Same as hsWcScopedTvs, but for a LHsSigType
 hsScopedTvs sig_ty
-  | HsIB { hsib_ext = HsIBRn { hsib_vars = vars }
+  | HsIB { hsib_ext = vars
          , hsib_body = sig_ty2 } <- sig_ty
   , L _ (HsForAllTy { hst_bndrs = tvs }) <- sig_ty2
   = vars ++ map hsLTyVarName tvs
@@ -1132,7 +1125,7 @@ splitLHsQualTy body              = (noLoc [], body)
 splitLHsInstDeclTy :: LHsSigType GhcRn
                    -> ([Name], LHsContext GhcRn, LHsType GhcRn)
 -- Split up an instance decl type, returning the pieces
-splitLHsInstDeclTy (HsIB { hsib_ext = HsIBRn { hsib_vars = itkvs }
+splitLHsInstDeclTy (HsIB { hsib_ext = itkvs
                          , hsib_body = inst_ty })
   | (tvs, cxt, body_ty) <- splitLHsSigmaTy inst_ty
   = (itkvs ++ map hsLTyVarName tvs, cxt, body_ty)
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 33e7c7d2b6..beb7c5b705 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -765,8 +765,7 @@ rnFamInstEqn doc mb_cls rhs_kvars
              all_fvs  = fvs `addOneFV` unLoc tycon'
                         -- type instance => use, hence addOneFV
 
-       ; return (HsIB { hsib_ext = HsIBRn { hsib_vars = all_ibs
-                                          , hsib_closed = True }
+       ; return (HsIB { hsib_ext = all_ibs
                       , hsib_body
                           = FamEqn { feqn_ext    = noExt
                                    , feqn_tycon  = tycon'
@@ -1691,7 +1690,7 @@ rnLDerivStrategy doc mds thing_inside
         NewtypeStrategy  -> boring_case (L loc NewtypeStrategy)
         ViaStrategy via_ty ->
           do (via_ty', fvs1) <- rnHsSigType doc via_ty
-             let HsIB { hsib_ext  = HsIBRn { hsib_vars = via_imp_tvs }
+             let HsIB { hsib_ext  = via_imp_tvs
                       , hsib_body = via_body } = via_ty'
                  (via_exp_tv_bndrs, _, _) = splitLHsSigmaTy via_body
                  via_exp_tvs = map hsLTyVarName via_exp_tv_bndrs
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index a9e02dc5a5..e5f51660da 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -127,7 +127,8 @@ rn_hs_sig_wc_type always_bind_free_tvs ctxt
        ; rnImplicitBndrs bind_free_tvs tv_rdrs $ \ vars ->
     do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
        ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = ib_ty' }
-             ib_ty'  = mk_implicit_bndrs vars hs_ty' fvs1
+             ib_ty'  = HsIB { hsib_ext = vars
+                            , hsib_body = hs_ty' }
        ; (res, fvs2) <- thing_inside sig_ty'
        ; return (res, fvs1 `plusFV` fvs2) } }
 rn_hs_sig_wc_type _ _ (HsWC _ (XHsImplicitBndrs _)) _
@@ -300,7 +301,9 @@ rnHsSigType ctx (HsIB { hsib_body = hs_ty })
        ; vars <- extractFilteredRdrTyVarsDups hs_ty
        ; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) vars $ \ vars ->
     do { (body', fvs) <- rnLHsType ctx hs_ty
-       ; return ( mk_implicit_bndrs vars body' fvs, fvs ) } }
+       ; return ( HsIB { hsib_ext = vars
+                       , hsib_body = body' }
+                , fvs ) } }
 rnHsSigType _ (XHsImplicitBndrs _) = panic "rnHsSigType"
 
 rnImplicitBndrs :: Bool    -- True <=> bring into scope any free type variables
@@ -367,18 +370,6 @@ rnLHsInstType :: SDoc -> LHsSigType GhcPs -> RnM (LHsSigType GhcRn, FreeVars)
 -- Do not try to decompose the inst_ty in case it is malformed
 rnLHsInstType doc inst_ty = rnHsSigType (GenericCtx doc) inst_ty
 
-mk_implicit_bndrs :: [Name]  -- implicitly bound
-                  -> a           -- payload
-                  -> FreeVars    -- FreeVars of payload
-                  -> HsImplicitBndrs GhcRn a
-mk_implicit_bndrs vars body fvs
-  = HsIB { hsib_ext = HsIBRn
-           { hsib_vars = vars
-           , hsib_closed = nameSetAll (not . isTyVarName) (vars `delFVs` fvs) }
-         , hsib_body = body }
-
-
-
 {- ******************************************************
 *                                                       *
            LHsType and HsType
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 37bfa18192..6f749fc60f 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -713,17 +713,14 @@ tcStandaloneDerivInstType
   :: UserTypeCtxt -> LHsSigWcType GhcRn
   -> TcM ([TyVar], DerivContext, Class, [Type])
 tcStandaloneDerivInstType ctxt
-    (HsWC { hswc_body = deriv_ty@(HsIB { hsib_ext = HsIBRn
-                                                        { hsib_vars   = vars
-                                                        , hsib_closed = closed }
+    (HsWC { hswc_body = deriv_ty@(HsIB { hsib_ext = vars
                                        , hsib_body   = deriv_ty_body })})
   | (tvs, theta, rho) <- splitLHsSigmaTy deriv_ty_body
   , L _ [wc_pred] <- theta
   , L _ (HsWildCardTy (AnonWildCard (L wc_span _))) <- ignoreParens wc_pred
   = do (deriv_tvs, _deriv_theta, deriv_cls, deriv_inst_tys)
          <- tcHsClsInstType ctxt $
-            HsIB { hsib_ext = HsIBRn { hsib_vars = vars
-                                     , hsib_closed = closed }
+            HsIB { hsib_ext = vars
                  , hsib_body
                      = L (getLoc deriv_ty_body) $
                        HsForAllTy { hst_bndrs = tvs
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index a5a900410f..8f4e1076ca 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -614,8 +614,10 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things
                        tvs
           _other    -> tvs `unionVarSet` id_tvs
         where
-           id_tvs = tyCoVarsOfType (idType id)
-           is_closed_type = not (anyVarSet isTyVar id_tvs)
+           id_ty          = idType id
+           id_tvs         = tyCoVarsOfType id_ty
+           id_co_tvs      = closeOverKinds (coVarsOfType id_ty)
+           is_closed_type = not (anyVarSet isTyVar (id_tvs `minusVarSet` id_co_tvs))
            -- We only care about being closed wrt /type/ variables
            -- E.g. a top-level binding might have a type like
            --          foo :: t |> co
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index efdda06fe3..4188303860 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -38,6 +38,7 @@ module TcHsType (
         tcHsLiftedTypeNC, tcHsOpenTypeNC,
         tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
         tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
+        failIfEmitsConstraints,
         solveEqualities, -- useful re-export
 
         typeLevelMode, kindLevelMode,
@@ -69,6 +70,7 @@ import TcUnify
 import TcIface
 import TcSimplify
 import TcHsSyn
+import TcErrors ( reportAllUnsolved )
 import TcType
 import Inst   ( tcInstTyBinders, tcInstTyBinder )
 import TyCoRep( TyBinder(..) )  -- Used in tcDataKindSig
@@ -178,7 +180,7 @@ tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
 
 kcHsSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
 kcHsSigType skol_info names (HsIB { hsib_body = hs_ty
-                                  , hsib_ext = HsIBRn { hsib_vars = sig_vars }})
+                                  , hsib_ext = sig_vars })
   = addSigCtxt (funsSigCtxt names) hs_ty $
     discardResult $
     tcImplicitTKBndrs skol_info sig_vars $
@@ -205,10 +207,7 @@ tcHsSigType ctxt sig_ty
               -- of kind * in a Template Haskell quote eg [t| Maybe |]
 
           -- Generalise here: see Note [Kind generalisation]
-       ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
-       ; ty <- if do_kind_gen
-               then tc_hs_sig_type_and_gen skol_info sig_ty kind >>= zonkTcType
-               else tc_hs_sig_type         skol_info sig_ty kind
+       ; ty <- tc_hs_sig_type_and_gen skol_info sig_ty kind >>= zonkTcType
 
        ; checkValidType ctxt ty
        ; traceTc "end tcHsSigType }" (ppr ty)
@@ -222,38 +221,23 @@ tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
 --   and then kind-generalizes.
 -- This will never emit constraints, as it uses solveEqualities interally.
 -- No validity checking or zonking
-tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
-                                              = HsIBRn { hsib_vars = sig_vars }
+tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext = sig_vars
                                        , hsib_body = hs_ty }) kind
-  = do { (tkvs, ty) <- solveEqualities $
-                       tcImplicitTKBndrs skol_info sig_vars $
-                       tc_lhs_type typeLevelMode hs_ty kind
-         -- NB the call to solveEqualities, which unifies all those
-         --    kind variables floating about, immediately prior to
-         --    kind generalisation
-
-       ; ty1 <- zonkPromoteType $ mkSpecForAllTys tkvs ty
-       ; kvs <- kindGeneralize ty1
+  = do { ((tkvs, ty), wanted) <- captureConstraints $
+                                 tcImplicitTKBndrs skol_info sig_vars $
+                                 tc_lhs_type typeLevelMode hs_ty kind
+         -- Any remaining variables (unsolved in the solveLocalEqualities in the
+         -- tcImplicitTKBndrs)
+         -- should be in the global tyvars, and therefore won't be quantified
+         -- over.
+
+       ; let ty1 = mkSpecForAllTys tkvs ty
+       ; kvs <- kindGeneralizeLocal wanted ty1
+       ; emitConstraints wanted -- we still need to solve these
        ; return (mkInvForAllTys kvs ty1) }
 
 tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
 
-tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
--- Kind-check/desugar a 'LHsSigType', but does not solve
--- the equalities that arise from doing so; instead it may
--- emit kind-equality constraints into the monad
--- Zonking, but no validity checking
-tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars }
-                               , hsib_body = hs_ty }) kind
-  = do { (tkvs, ty) <- tcImplicitTKBndrs skol_info sig_vars $
-                       tc_lhs_type typeLevelMode hs_ty kind
-
-          -- need to promote any remaining metavariables; test case:
-          -- dependent/should_fail/T14066e.
-       ; zonkPromoteType (mkSpecForAllTys tkvs ty) }
-
-tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
-
 -----------------
 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
@@ -330,7 +314,14 @@ tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
 -- Like tcHsSigType, but for a class instance declaration
 tcHsClsInstType user_ctxt hs_inst_ty
   = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
-    do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
+    {- We want to fail here if the tc_hs_sig_type_and_gen emits constraints.
+       First off, we know we'll never solve the constraints, as classes are
+       always at top level, and their constraints do not inform the kind checking
+       of method types. So failing isn't wrong. Yet, the reason we do it is
+       to avoid the validity checker from seeing unsolved coercion holes in
+       types. Much better just to report the kind error directly. -}
+    do { inst_ty <- failIfEmitsConstraints $
+                    tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
        ; inst_ty <- zonkTcTypeToType emptyZonkEnv inst_ty
        ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
 
@@ -345,6 +336,12 @@ tcHsTypeApp wc_ty kind
                -- signature so we want to solve its equalities right now
                tcWildCardBinders sig_wcs $ \ _ ->
                tcCheckLHsType hs_ty kind
+       -- We must promote here. Ex:
+       --   f :: forall a. a
+       --   g = f @(forall b. Proxy b -> ()) @Int ...
+       -- After when processing the @Int, we'll have to check its kind
+       -- against the as-yet-unknown kind of b. This check causes an assertion
+       -- failure if we don't promote.
        ; ty <- zonkPromoteType ty
        ; checkValidType TypeAppCtxt ty
        ; return ty }
@@ -392,50 +389,7 @@ tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty)
   where
     mode = allowUnsaturated typeLevelMode
 
----------------------------
--- | Should we generalise the kind of this type signature?
--- We *should* generalise if the type is closed
--- or if NoMonoLocalBinds is set. Otherwise, nope.
--- See Note [Kind generalisation plan]
-decideKindGeneralisationPlan :: LHsSigType GhcRn -> TcM Bool
-decideKindGeneralisationPlan sig_ty@(HsIB { hsib_ext
-                                            = HsIBRn { hsib_closed = closed } })
-  = do { mono_locals <- xoptM LangExt.MonoLocalBinds
-       ; let should_gen = not mono_locals || closed
-       ; traceTc "decideKindGeneralisationPlan"
-           (ppr sig_ty $$ text "should gen?" <+> ppr should_gen)
-       ; return should_gen }
-decideKindGeneralisationPlan(XHsImplicitBndrs _)
-  = panic "decideKindGeneralisationPlan"
-
-{- Note [Kind generalisation plan]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When should we do kind-generalisation for user-written type signature?
-Answer: we use the same rule as for value bindings:
-
- * We always kind-generalise if the type signature is closed
- * Additionally, we attempt to generalise if we have NoMonoLocalBinds
-
-Trac #13337 shows the problem if we kind-generalise an open type (i.e.
-one that mentions in-scope type variable
-  foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
-      => proxy a -> String
-  foo _ = case eqT :: Maybe (k :~: Type) of
-            Nothing   -> ...
-            Just Refl -> case eqT :: Maybe (a :~: Int) of ...
-
-In the expression type sig on the last line, we have (a :: k)
-but (Int :: Type).  Since (:~:) is kind-homogeneous, this requires
-k ~ *, which is true in the Refl branch of the outer case.
-
-That equality will be solved if we allow it to float out to the
-implication constraint for the Refl match, but not not if we aggressively
-attempt to solve all equalities the moment they occur; that is, when
-checking (Maybe (a :~: Int)).   (NB: solveEqualities fails unless it
-solves all the kind equalities, which is the right thing at top level.)
-
-So here the right thing is simply not to do kind generalisation!
-
+{-
 ************************************************************************
 *                                                                      *
       Type-checking modes
@@ -1495,9 +1449,10 @@ Checking a user-written signature requires several steps:
 
  1. Generate constraints.
  2. Solve constraints.
- 3. Zonk and promote tyvars.
- 4. (Optional) Kind-generalize.
- 5. Check validity.
+ 3. Zonk.
+ 4. Promote tyvars and/or kind-generalize.
+ 5. Zonk.
+ 6. Check validity.
 
 There may be some surprises in here:
 
@@ -1507,12 +1462,34 @@ to get these in the right order (see Note [Keeping scoped variables in
 order: Implicit]). Additionally, solving is necessary in order to
 kind-generalize correctly.
 
-Step 3 requires *promoting* type variables. If there are any foralls
-in a type, the TcLevel will be bumped within the forall. This might
-lead to the generation of matavars with a high level. If we don't promote,
-we violate MetaTvInv of Note [TcLevel and untouchable type variables]
+In Step 4, we have to deal with the fact that metatyvars generated
+in the type may have a bumped TcLevel, because explicit foralls
+raise the TcLevel. To avoid these variables from every being visible
+in the surrounding context, we must obey the following dictum:
+
+  Every metavariable in a type must either be
+    (A) promoted, or
+    (B) generalized.
+
+If a variable is generalized, then it becomes a skolem and no longer
+has a proper TcLevel. (I'm ignoring the TcLevel on a skolem here, as
+it's not really in play here.) On the other hand, if it is not
+generalized (because we're not generalizing the construct -- e.g., pattern
+sig -- or because the metavars are constrained -- see kindGeneralizeLocal)
+we need to promote to (MetaTvInv) of Note [TcLevel and untouchable type variables]
 in TcType.
 
+After promoting/generalizing, we need to zonk *again* because both
+promoting and generalizing fill in metavariables.
+
+To avoid the double-zonk, we do two things:
+ 1. zonkPromoteType and friends zonk and promote at the same time.
+    Accordingly, the function does setps 3-5 all at once, preventing
+    the need for multiple traversals.
+
+ 2. kindGeneralize does not require a zonked type -- it zonks as it
+    gathers free variables. So this way effectively sidesteps step 3.
+
 -}
 
 tcWildCardBinders :: [Name]
@@ -1921,14 +1898,36 @@ kindGeneralize :: TcType -> TcM [KindVar]
 -- Quantify the free kind variables of a kind or type
 -- In the latter case the type is closed, so it has no free
 -- type variables.  So in both cases, all the free vars are kind vars
--- Input must be zonked.
+-- Input needn't be zonked.
 -- NB: You must call solveEqualities or solveLocalEqualities before
 -- kind generalization
-kindGeneralize kind_or_type
-  = do { let kvs = tyCoVarsOfTypeDSet kind_or_type
-             dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
+kindGeneralize = kindGeneralizeLocal emptyWC
+
+-- | This variant of 'kindGeneralize' refuses to generalize over any
+-- variables free in the given WantedConstraints. Instead, it promotes
+-- these variables into an outer TcLevel. See also
+-- Note [Promoting unification variables] in TcSimplify
+kindGeneralizeLocal :: WantedConstraints -> TcType -> TcM [KindVar]
+kindGeneralizeLocal wanted kind_or_type
+  = do {
+       -- This bit is very much like decideMonoTyVars in TcSimplify,
+       -- but constraints are so much simpler in kinds, it is much
+       -- easier here. (In particular, we never quantify over a
+       -- constraint in a type.)
+       ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
+       ; (_, constrained) <- promoteTyVarSet constrained
+
+         -- NB: zonk here, after promotion
+       ; kvs <- zonkTcTypeAndFV kind_or_type
+       ; let dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
+
        ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
-       ; quantifyTyVars gbl_tvs dvs }
+       ; traceTc "kindGeneralizeLocal" (vcat [ ppr wanted
+                                             , ppr kind_or_type
+                                             , ppr constrained
+                                             , ppr dvs ])
+
+       ; quantifyTyVars (gbl_tvs `unionVarSet` constrained) dvs }
 
 {-
 Note [Kind generalisation]
@@ -2268,7 +2267,7 @@ tcHsPartialSigType
 -- See Note [Recipe for checking a signature]
 tcHsPartialSigType ctxt sig_ty
   | HsWC { hswc_ext  = sig_wcs,         hswc_body = ib_ty } <- sig_ty
-  , HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_hs_tvs }
+  , HsIB { hsib_ext = implicit_hs_tvs
          , hsib_body = hs_ty } <- ib_ty
   , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
   = addSigCtxt ctxt hs_ty $
@@ -2392,7 +2391,7 @@ tcHsPatSigType :: UserTypeCtxt
 -- See Note [Recipe for checking a signature]
 tcHsPatSigType ctxt sig_ty
   | HsWC { hswc_ext = sig_wcs,   hswc_body = ib_ty } <- sig_ty
-  , HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars}
+  , HsIB { hsib_ext = sig_vars
          , hsib_body = hs_ty } <- ib_ty
   = addSigCtxt ctxt hs_ty $
     do { sig_tkvs <- mapM new_implicit_tv sig_vars
@@ -2406,6 +2405,9 @@ tcHsPatSigType ctxt sig_ty
 
           -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
           -- contains a forall). Promote these.
+          -- Ex: f (x :: forall a. Proxy a -> ()) = ... x ...
+          -- When we instantiate x, we have to compare the kind of the argument
+          -- to a's kind, which will be a metavariable.
         ; sig_ty <- zonkPromoteType sig_ty
         ; checkValidType ctxt sig_ty
 
@@ -2582,7 +2584,7 @@ unifyKinds rn_tys act_kinds
 -- to make sure that any free meta-tyvars in the type are promoted to the
 -- current TcLevel. (They might be at a higher level due to the level-bumping
 -- in tcExplicitTKBndrs, for example.) This function both zonks *and*
--- promotes.
+-- promotes. Why at the same time? See Note [Recipe for checking a signature]
 zonkPromoteType :: TcType -> TcM TcType
 zonkPromoteType = mapType zonkPromoteMapper ()
 
@@ -2618,10 +2620,8 @@ zonkPromoteTcTyVar tv
   = do { let ref = metaTyVarRef tv
        ; contents <- readTcRef ref
        ; case contents of
-           Flexi -> do { promoted <- promoteTyVar tv
-                       ; if promoted
-                         then zonkPromoteTcTyVar tv   -- read it again
-                         else mkTyVarTy <$> zonkPromoteTyCoVarKind tv }
+           Flexi -> do { (_, promoted_tv) <- promoteTyVar tv
+                       ; mkTyVarTy <$> zonkPromoteTyCoVarKind promoted_tv }
            Indirect ty -> zonkPromoteType ty }
 
   | isTcTyVar tv && isSkolemTyVar tv  -- NB: isSkolemTyVar says "True" to pure TyVars
@@ -2667,6 +2667,7 @@ tcLHsKindSig ctxt hs_kind
   = do { kind <- solveLocalEqualities $
                  tc_lhs_kind kindLevelMode hs_kind
        ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
+       -- No generalization, so we must promote
        ; kind <- zonkPromoteType kind
          -- This zonk is very important in the case of higher rank kinds
          -- E.g. Trac #13879    f :: forall (p :: forall z (y::z). <blah>).
@@ -2762,3 +2763,14 @@ reportFloatingKvs tycon_name flav all_tvs bad_tvs
 
     ppr_tv_bndrs tvs = sep (map pp_tv tvs)
     pp_tv tv         = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv))
+
+-- | If the inner action emits constraints, reports them as errors and fails;
+-- otherwise, propagates the return value. Useful as a wrapper around
+-- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be
+-- another chance to solve constraints
+failIfEmitsConstraints :: TcM a -> TcM a
+failIfEmitsConstraints thing_inside
+  = do { (res, lie) <- captureConstraints thing_inside
+       ; reportAllUnsolved lie
+       ; return res
+       }
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 9a94365233..cd6aec729b 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -588,9 +588,8 @@ tcDataFamInstDecl :: Maybe ClsInstInfo
                   -> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
   -- "newtype instance" and "data instance"
 tcDataFamInstDecl mb_clsinfo
-    (L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext
-                                               = HsIBRn { hsib_vars = tv_names }
-                                 , hsib_body =
+    (L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext = tv_names
+                                                   , hsib_body =
       FamEqn { feqn_pats   = pats
              , feqn_tycon  = fam_tc_name
              , feqn_fixity = fixity
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 58138eb631..80929d12d4 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1307,6 +1307,8 @@ a \/\a in the final result but all the occurrences of a will be zonked to ()
 -- variables free in anything (term-level or type-level) in scope. We thus
 -- don't have to worry about clashes with things that are not in scope, because
 -- if they are reachable, then they'll be returned here.
+-- NB: This is closed over kinds, so it can return unification variables mentioned
+-- in the kinds of in-scope tyvars.
 tcGetGlobalTyCoVars :: TcM TcTyVarSet
 tcGetGlobalTyCoVars
   = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index c8e168dea7..4449d67c29 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -391,14 +391,14 @@ tcRnSrcDecls :: Bool  -- False => no 'module M(..) where' header at all
              -> TcM TcGblEnv
 tcRnSrcDecls explicit_mod_hdr decls
  = do { -- Do all the declarations
-      ; ((tcg_env, tcl_env), lie) <- captureTopConstraints $
-              do { (tcg_env, tcl_env) <- tc_rn_src_decls decls
+      ; (tcg_env, tcl_env, lie) <- tc_rn_src_decls decls
 
-                   -- Check for the 'main' declaration
-                   -- Must do this inside the captureTopConstraints
-                 ; tcg_env <- setEnvs (tcg_env, tcl_env) $
-                              checkMain explicit_mod_hdr
-                 ; return (tcg_env, tcl_env) }
+        -- Check for the 'main' declaration
+        -- Must do this inside the captureTopConstraints
+      ; (tcg_env, lie_main) <- setEnvs (tcg_env, tcl_env) $
+                               -- always set envs *before* captureTopConstraints
+                               captureTopConstraints $
+                               checkMain explicit_mod_hdr
 
       ; setEnvs (tcg_env, tcl_env) $ do {
 
@@ -412,7 +412,7 @@ tcRnSrcDecls explicit_mod_hdr decls
              --  * the local env exposes the local Ids to simplifyTop,
              --    so that we get better error messages (monomorphism restriction)
       ; new_ev_binds <- {-# SCC "simplifyTop" #-}
-                        simplifyTop lie
+                        simplifyTop (lie `andWC` lie_main)
 
         -- Emit Typeable bindings
       ; tcg_env <- mkTypeableBinds
@@ -470,16 +470,17 @@ run_th_modfinalizers = do
   then getEnvs
   else do
     writeTcRef th_modfinalizers_var []
-    (envs, lie) <- captureTopConstraints $ do
-      sequence_ th_modfinalizers
-      -- Finalizers can add top-level declarations with addTopDecls.
-      tc_rn_src_decls []
-    setEnvs envs $ do
+    (_, lie_th) <- captureTopConstraints $
+                   sequence_ th_modfinalizers
+      -- Finalizers can add top-level declarations with addTopDecls, so
+      -- we have to run tc_rn_src_decls to get them
+    (tcg_env, tcl_env, lie_top_decls) <- tc_rn_src_decls []
+    setEnvs (tcg_env, tcl_env) $ do
       -- Subsequent rounds of finalizers run after any new constraints are
       -- simplified, or some types might not be complete when using reify
       -- (see #12777).
       new_ev_binds <- {-# SCC "simplifyTop2" #-}
-                      simplifyTop lie
+                      simplifyTop (lie_th `andWC` lie_top_decls)
       updGblEnv (\tcg_env ->
         tcg_env { tcg_ev_binds = tcg_ev_binds tcg_env `unionBags` new_ev_binds }
         )
@@ -487,9 +488,10 @@ run_th_modfinalizers = do
         run_th_modfinalizers
 
 tc_rn_src_decls :: [LHsDecl GhcPs]
-                -> TcM (TcGblEnv, TcLclEnv)
+                -> TcM (TcGblEnv, TcLclEnv, WantedConstraints)
 -- Loops around dealing with each top level inter-splice group
 -- in turn, until it's dealt with the entire module
+-- Never emits constraints; calls captureTopConstraints internally
 tc_rn_src_decls ds
  = {-# SCC "tc_rn_src_decls" #-}
    do { (first_group, group_tail) <- findSplice ds
@@ -534,13 +536,17 @@ tc_rn_src_decls ds
                     }
 
       -- Type check all declarations
-      ; (tcg_env, tcl_env) <- setGblEnv tcg_env $
-                              tcTopSrcDecls rn_decls
+      -- NB: set the env **before** captureTopConstraints so that error messages
+      -- get reported w.r.t. the right GlobalRdrEnv. It is for this reason that
+      -- the captureTopConstraints must go here, not in tcRnSrcDecls.
+      ; ((tcg_env, tcl_env), lie1) <- setGblEnv tcg_env $
+                                      captureTopConstraints $
+                                      tcTopSrcDecls rn_decls
 
         -- If there is no splice, we're nearly done
       ; setEnvs (tcg_env, tcl_env) $
         case group_tail of
-          { Nothing -> return (tcg_env, tcl_env)
+          { Nothing -> return (tcg_env, tcl_env, lie1)
 
             -- If there's a splice, we must carry on
           ; Just (SpliceDecl _ (L loc splice) _, rest_ds) ->
@@ -551,8 +557,11 @@ tc_rn_src_decls ds
                                                              splice)
 
                  -- Glue them on the front of the remaining decls and loop
-               ; setGblEnv (tcg_env `addTcgDUs` usesOnly splice_fvs) $
-                 tc_rn_src_decls (spliced_decls ++ rest_ds)
+               ; (tcg_env, tcl_env, lie2) <-
+                   setGblEnv (tcg_env `addTcgDUs` usesOnly splice_fvs) $
+                   tc_rn_src_decls (spliced_decls ++ rest_ds)
+
+               ; return (tcg_env, tcl_env, lie1 `andWC` lie2)
                }
           ; Just (XSpliceDecl _, _) -> panic "tc_rn_src_decls"
           }
@@ -583,8 +592,9 @@ tcRnHsBootDecls hsc_src decls
               <- rnTopSrcDecls first_group
         -- The empty list is for extra dependencies coming from .hs-boot files
         -- See Note [Extra dependencies from .hs-boot files] in RnSource
-        ; (gbl_env, lie) <- captureTopConstraints $ setGblEnv tcg_env $ do {
-
+        ; (gbl_env, lie) <- setGblEnv tcg_env $ captureTopConstraints $ do {
+              -- NB: setGblEnv **before** captureTopConstraints so that
+              -- if the latter reports errors, it knows what's in scope
 
                 -- Check for illegal declarations
         ; case group_tail of
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 13b5e7ad48..4f4d9b0f82 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -303,12 +303,12 @@ tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
 -- See Note [Pattern synonym signatures]
 -- See Note [Recipe for checking a signature] in TcHsType
 tcPatSynSig name sig_ty
-  | HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_hs_tvs }
+  | HsIB { hsib_ext = implicit_hs_tvs
          , hsib_body = hs_ty }  <- sig_ty
   , (univ_hs_tvs, hs_req,  hs_ty1)     <- splitLHsSigmaTy hs_ty
   , (ex_hs_tvs,   hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1
   = do { (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
-           <-  -- NB: tcImplicitTKBndrs calls solveEqualities
+           <-  -- NB: tcImplicitTKBndrs calls solveLocalEqualities
               tcImplicitTKBndrs skol_info implicit_hs_tvs $
               tcExplicitTKBndrs skol_info univ_hs_tvs     $
               tcExplicitTKBndrs skol_info ex_hs_tvs       $
@@ -319,9 +319,8 @@ tcPatSynSig name sig_ty
                      -- e.g. pattern Zero <- 0#   (Trac #12094)
                  ; return (req, prov, body_ty) }
 
-       ; ungen_patsyn_ty <- zonkPromoteType $
-                            build_patsyn_type [] implicit_tvs univ_tvs req
-                                              ex_tvs prov body_ty
+       ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvs req
+                                                 ex_tvs prov body_ty
 
        -- Kind generalisation
        ; kvs <- kindGeneralize ungen_patsyn_ty
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 5856c0f14b..7ea19b4e6c 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -5,12 +5,14 @@ module TcSimplify(
        growThetaTyVars,
        simplifyAmbiguityCheck,
        simplifyDefault,
-       simplifyTop, simplifyTopImplic, captureTopConstraints,
+       simplifyTop, simplifyTopImplic,
        simplifyInteractive,
        solveEqualities, solveLocalEqualities,
        simplifyWantedsTcM,
        tcCheckSatisfiability,
 
+       captureTopConstraints,
+
        simpl_top,
 
        promoteTyVar,
@@ -76,6 +78,8 @@ captureTopConstraints :: TcM a -> TcM (a, WantedConstraints)
 -- generates plus the constraints produced by static forms inside.
 -- If it fails with an exception, it reports any insolubles
 -- (out of scope variables) before doing so
+-- NB: bring any environments into scope before calling this, so that
+-- the reportUnsolved has access to the most complete GlobalRdrEnv
 captureTopConstraints thing_inside
   = do { static_wc_var <- TcM.newTcRef emptyWC ;
        ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $
@@ -1027,7 +1031,7 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
   = do {  -- Promote any tyvars that we cannot generalise
           -- See Note [Promote momomorphic tyvars]
        ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
-       ; prom <- promoteTyVarSet mono_tvs
+       ; (prom, _) <- promoteTyVarSet mono_tvs
 
        -- Default any kind/levity vars
        ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
@@ -1909,10 +1913,11 @@ we'll get more Givens (a unification is like adding a Given) to
 allow the implication to make progress.
 -}
 
-promoteTyVar :: TcTyVar -> TcM Bool
+promoteTyVar :: TcTyVar -> TcM (Bool, TcTyVar)
 -- When we float a constraint out of an implication we must restore
 -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
 -- Return True <=> we did some promotion
+-- Also returns either the original tyvar (no promotion) or the new one
 -- See Note [Promoting unification variables]
 promoteTyVar tv
   = do { tclvl <- TcM.getTcLevel
@@ -1920,14 +1925,16 @@ promoteTyVar tv
          then do { cloned_tv <- TcM.cloneMetaTyVar tv
                  ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
                  ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
-                 ; return True }
-         else return False }
+                 ; return (True, rhs_tv) }
+         else return (False, tv) }
 
 -- Returns whether or not *any* tyvar is defaulted
-promoteTyVarSet :: TcTyVarSet -> TcM Bool
+promoteTyVarSet :: TcTyVarSet -> TcM (Bool, TcTyVarSet)
 promoteTyVarSet tvs
-  = or <$> mapM promoteTyVar (nonDetEltsUniqSet tvs)
-    -- non-determinism is OK because order of promotion doesn't matter
+  = do { (bools, tyvars) <- mapAndUnzipM promoteTyVar (nonDetEltsUniqSet tvs)
+           -- non-determinism is OK because order of promotion doesn't matter
+
+       ; return (or bools, mkVarSet tyvars) }
 
 promoteTyVarTcS :: TcTyVar  -> TcS ()
 -- When we float a constraint out of an implication we must restore
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 5e50dac3f3..b0d68152f6 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1180,7 +1180,7 @@ reifyInstances th_nm th_tys
                do { (rn_ty, fvs) <- rnLHsType doc rdr_ty
                   ; return ((tv_names, rn_ty), fvs) }
         ; (_tvs, ty)
-            <- solveEqualities $
+            <- failIfEmitsConstraints $  -- avoid error cascade if there are unsolved
                tcImplicitTKBndrs ReifySkol tv_names $
                fst <$> tcLHsType rn_ty
         ; ty <- zonkTcTypeToType emptyZonkEnv ty
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 8a3b7c7946..cd80be649c 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1399,7 +1399,7 @@ but it works.
 -------------------------
 kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
 kcTyFamInstEqn tc_fam_tc
-    (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
+    (L loc (HsIB { hsib_ext = tv_names
                  , hsib_body = FamEqn { feqn_tycon  = L _ eqn_tc_name
                                       , feqn_pats   = pats
                                       , feqn_rhs    = hs_ty }}))
@@ -1452,7 +1452,7 @@ tcTyFamInstEqn :: TcTyCon -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
 -- Needs to be here, not in TcInstDcls, because closed families
 -- (typechecked here) have TyFamInstEqns
 tcTyFamInstEqn fam_tc mb_clsinfo
-    (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
+    (L loc (HsIB { hsib_ext = tv_names
                  , hsib_body = FamEqn { feqn_tycon  = L _ eqn_tc_name
                                       , feqn_pats   = pats
                                       , feqn_rhs    = hs_ty }}))
@@ -1960,7 +1960,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
              skol_info      = DataConSkol name
 
        ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
-           <- solveEqualities $
+           <- failIfEmitsConstraints $  -- we won't get another crack, and we don't
+                                        -- want an error cascade
               tcImplicitTKBndrs skol_info implicit_tkv_nms $
               tcExplicitTKBndrs skol_info explicit_tkv_nms $
               do { ctxt <- tcHsMbContext cxt
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 1dc60e7312..7c9ef67837 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -2095,6 +2095,7 @@ checkValidTelescope tvbs user_tyvars extra
 -}
 
 -- Free variables of a type, retaining repetitions, and expanding synonyms
+-- This ignores coercions, as coercions aren't user-written
 fvType :: Type -> [TyCoVar]
 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
 fvType (TyVarTy tv)          = [tv]
@@ -2105,42 +2106,12 @@ fvType (FunTy arg res)       = fvType arg ++ fvType res
 fvType (ForAllTy (TvBndr tv _) ty)
   = fvType (tyVarKind tv) ++
     filter (/= tv) (fvType ty)
-fvType (CastTy ty co)        = fvType ty ++ fvCo co
-fvType (CoercionTy co)       = fvCo co
+fvType (CastTy ty _)         = fvType ty
+fvType (CoercionTy {})       = []
 
 fvTypes :: [Type] -> [TyVar]
 fvTypes tys                = concat (map fvType tys)
 
-fvMCo :: MCoercion -> [TyCoVar]
-fvMCo MRefl    = []
-fvMCo (MCo co) = fvCo co
-
-fvCo :: Coercion -> [TyCoVar]
-fvCo (Refl ty)              = fvType ty
-fvCo (GRefl _ ty mco)       = fvType ty ++ fvMCo mco
-fvCo (TyConAppCo _ _ args)  = concatMap fvCo args
-fvCo (AppCo co arg)         = fvCo co ++ fvCo arg
-fvCo (ForAllCo tv h co)     = filter (/= tv) (fvCo co) ++ fvCo h
-fvCo (FunCo _ co1 co2)      = fvCo co1 ++ fvCo co2
-fvCo (CoVarCo v)            = [v]
-fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
-fvCo (UnivCo p _ t1 t2)     = fvProv p ++ fvType t1 ++ fvType t2
-fvCo (SymCo co)             = fvCo co
-fvCo (TransCo co1 co2)      = fvCo co1 ++ fvCo co2
-fvCo (NthCo _ _ co)         = fvCo co
-fvCo (LRCo _ co)            = fvCo co
-fvCo (InstCo co arg)        = fvCo co ++ fvCo arg
-fvCo (KindCo co)            = fvCo co
-fvCo (SubCo co)             = fvCo co
-fvCo (AxiomRuleCo _ cs)     = concatMap fvCo cs
-fvCo (HoleCo h)             = pprPanic "fvCo falls into a hole" (ppr h)
-
-fvProv :: UnivCoProvenance -> [TyCoVar]
-fvProv UnsafeCoerceProv    = []
-fvProv (PhantomProv co)    = fvCo co
-fvProv (ProofIrrelProv co) = fvCo co
-fvProv (PluginProv _)      = []
-
 sizeType :: Type -> Int
 -- Size of a type: the number of variables and constructors
 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
@@ -2151,7 +2122,7 @@ sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
 sizeType (ForAllTy _ ty)   = sizeType ty
 sizeType (CastTy ty _)     = sizeType ty
-sizeType (CoercionTy _)    = 1
+sizeType (CoercionTy _)    = 0
 
 sizeTypes :: [Type] -> Int
 sizeTypes = foldr ((+) . sizeType) 0
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 3ea4f61741..fd3d1dfff7 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -2247,6 +2247,34 @@ sym (ForAllCo tv h g)
 ==>
 ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])
 
+Note [Substituting in a coercion hole]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It seems highly suspicious to be substituting in a coercion that still
+has coercion holes. Yet, this can happen in a situation like this:
+
+  f :: forall k. k :~: Type -> ()
+  f Refl = let x :: forall (a :: k). [a] -> ...
+               x = ...
+
+When we check x's type signature, we require that k ~ Type. We indeed
+know this due to the Refl pattern match, but the eager unifier can't
+make use of givens. So, when we're done looking at x's type, a coercion
+hole will remain. Then, when we're checking x's definition, we skolemise
+x's type (in order to, e.g., bring the scoped type variable `a` into scope).
+This requires performing a substitution for the fresh skolem variables.
+
+This subsitution needs to affect the kind of the coercion hole, too --
+otherwise, the kind will have an out-of-scope variable in it. More problematically
+in practice (we won't actually notice the out-of-scope variable ever), skolems
+in the kind might have too high a level, triggering a failure to uphold the
+invariant that no free variables in a type have a higher level than the
+ambient level in the type checker. In the event of having free variables in the
+hole's kind, I'm pretty sure we'll always have an erroneous program, so we
+don't need to worry what will happen when the hole gets filled in. After all,
+a hole relating a locally-bound type variable will be unable to be solved. This
+is why it's OK not to look through the IORef of a coercion hole during
+substitution.
+
 -}
 
 -- | Type substitution, see 'zipTvSubst'
@@ -2511,19 +2539,17 @@ subst_co subst co
     go (SubCo co)            = mkSubCo $! (go co)
     go (AxiomRuleCo c cs)    = let cs1 = map go cs
                                 in cs1 `seqList` AxiomRuleCo c cs1
-    go (HoleCo h)            = HoleCo h
-      -- NB: this last case is a little suspicious, but we need it. Originally,
-      -- there was a panic here, but it triggered from deeplySkolemise. Because
-      -- we only skolemise tyvars that are manually bound, this operation makes
-      -- sense, even over a coercion with holes.  We don't need to substitute
-      -- in the type of the coHoleCoVar because it wouldn't makes sense to have
-      --    forall a. ....(ty |> {hole_cv::a})....
+    go (HoleCo h)            = HoleCo $! go_hole h
 
     go_prov UnsafeCoerceProv     = UnsafeCoerceProv
     go_prov (PhantomProv kco)    = PhantomProv (go kco)
     go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
     go_prov p@(PluginProv _)     = p
 
+    -- See Note [Substituting in a coercion hole]
+    go_hole h@(CoercionHole { ch_co_var = cv })
+      = h { ch_co_var = updateVarType go_ty cv }
+
 substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion)
 substForAllCoBndr subst
   = substForAllCoBndrUsing False (substCo subst) subst
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 5d1c0b30cb..d5cdf71ed0 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -10559,49 +10559,6 @@ and :extension:`GADTs`. You can switch it off again with
 :extension:`NoMonoLocalBinds <-XMonoLocalBinds>` but type inference becomes
 less predictable if you do so. (Read the papers!)
 
-.. _kind-generalisation:
-
-Kind generalisation
--------------------
-
-Just as :extension:`MonoLocalBinds` places limitations on when the *type* of a
-*term* is generalised (see :ref:`mono-local-binds`), it also limits when the
-*kind* of a *type signature* is generalised. Here is an example involving
-:ref:`type signatures on instance declarations <instance-sigs>`: ::
-
-    data Proxy a = Proxy
-    newtype Tagged s b = Tagged b
-
-    class C b where
-      c :: forall (s :: k). Tagged s b
-
-    instance C (Proxy a) where
-      c :: forall s. Tagged s (Proxy a)
-      c = Tagged Proxy
-
-With :extension:`MonoLocalBinds` enabled, this ``C (Proxy a)`` instance will
-fail to typecheck. The reason is that the type signature for ``c`` captures
-``a``, an outer-scoped type variable, which means the type signature is not
-closed. Therefore, the inferred kind for ``s`` will *not* be generalised, and
-as a result, it will fail to unify with the kind variable ``k`` which is
-specified in the declaration of ``c``. This can be worked around by specifying
-an explicit kind variable for ``s``, e.g., ::
-
-    instance C (Proxy a) where
-      c :: forall (s :: k). Tagged s (Proxy a)
-      c = Tagged Proxy
-
-or, alternatively: ::
-
-    instance C (Proxy a) where
-      c :: forall k (s :: k). Tagged s (Proxy a)
-      c = Tagged Proxy
-
-This declarations are equivalent using Haskell's implicit "add implicit
-foralls" rules (see :ref:`implicit-quantification`). The implicit foralls rules
-are purely syntactic and are quite separate from the kind generalisation
-described here.
-
 .. _visible-type-application:
 
 Visible type application
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_compile/T14066h.hs
index a20ae30958..df3db1c15d 100644
--- a/testsuite/tests/dependent/should_fail/T14066h.hs
+++ b/testsuite/tests/dependent/should_compile/T14066h.hs
@@ -7,5 +7,5 @@ import Data.Proxy
 f :: forall b. b -> (Proxy Int, Proxy Maybe)
 f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
   where
-    y :: (Proxy a, b)  -- MonoLocalBinds means this won't generalize over the kind of a
+    y :: (Proxy a, b)  -- this generalizes over the kind of a
     y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 4e096c1f71..418fba2d85 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -53,3 +53,4 @@ test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
 test('T15346', normal, compile, [''])
 test('T15419', normal, compile, [''])
+test('T14066h', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr
index 630f010fa3..a8e64d4e0c 100644
--- a/testsuite/tests/dependent/should_fail/DepFail1.stderr
+++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr
@@ -2,11 +2,25 @@
 DepFail1.hs:7:6: error:
     • Expecting one more argument to ‘Proxy Bool’
       Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’
-    • In the type signature:
-        z :: Proxy Bool
+    • In the type signature: z :: Proxy Bool
+
+DepFail1.hs:8:5: error:
+    • Couldn't match expected type ‘Proxy Bool’
+                  with actual type ‘Proxy k0 a1’
+    • In the expression: P
+      In an equation for ‘z’: z = P
 
 DepFail1.hs:10:16: error:
     • Expected kind ‘Int’, but ‘Bool’ has kind ‘*’
     • In the second argument of ‘Proxy’, namely ‘Bool’
-      In the type signature:
-        a :: Proxy Int Bool
+      In the type signature: a :: Proxy Int Bool
+
+DepFail1.hs:11:5: error:
+    • Couldn't match kind ‘*’ with ‘Int’
+      When matching types
+        a0 :: Int
+        Bool :: *
+      Expected type: Proxy Int Bool
+        Actual type: Proxy Int a0
+    • In the expression: P
+      In an equation for ‘a’: a = P
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
index 0ae1710bf0..3e8bef6858 100644
--- a/testsuite/tests/dependent/should_fail/T13895.stderr
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -1,4 +1,28 @@
 
+T13895.hs:8:14: error:
+    • Could not deduce (Typeable (t dict0))
+      from the context: (Data a, Typeable (t dict))
+        bound by the type signature for:
+                   dataCast1 :: forall k (dict :: Typeable k) (dict1 :: Typeable
+                                                                          *) a (c :: *
+                                                                                     -> *) (t :: forall k1.
+                                                                                                 Typeable
+                                                                                                   k1 =>
+                                                                                                 k1
+                                                                                                 -> *).
+                                (Data a, Typeable (t dict)) =>
+                                (forall d. Data d => c (t dict1 d)) -> Maybe (c a)
+        at T13895.hs:(8,14)-(14,24)
+      The type variable ‘dict0’ is ambiguous
+    • In the ambiguity check for ‘dataCast1’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
+        dataCast1 :: forall (a :: Type).
+                     Data a =>
+                     forall (c :: Type -> Type)
+                            (t :: forall (k :: Type). Typeable k => k -> Type).
+                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
 T13895.hs:12:23: error:
     • Illegal constraint in a kind: Typeable k0
     • In the first argument of ‘Typeable’, namely ‘t’
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
index cd0142f5c1..e5179e510b 100644
--- a/testsuite/tests/dependent/should_fail/T14066.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -1,6 +1,6 @@
 
 T14066.hs:15:59: error:
-    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • Expected kind ‘k’, but ‘b’ has kind ‘k1’
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature: g :: forall k (b :: k). SameKind a b
       In the expression:
@@ -8,4 +8,6 @@ T14066.hs:15:59: error:
           g :: forall k (b :: k). SameKind a b
           g = undefined
         in ()
-    • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4)
+    • Relevant bindings include
+        x :: Proxy a (bound at T14066.hs:15:4)
+        f :: Proxy a -> () (bound at T14066.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
index 504ca5a80e..193c74d193 100644
--- a/testsuite/tests/dependent/should_fail/T14066e.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -1,6 +1,15 @@
 
 T14066e.hs:13:59: error:
-    • Expected kind ‘c’, but ‘b'’ has kind ‘k0’
+    • Couldn't match kind ‘k1’ with ‘*’
+      ‘k1’ is a rigid type variable bound by
+        the type signature for:
+          j :: forall k k1 (c :: k1) (b :: k).
+               Proxy a -> Proxy b -> Proxy c -> Proxy b
+        at T14066e.hs:12:5-61
+      When matching kinds
+        k :: *
+        c :: k1
+      Expected kind ‘c’, but ‘b'’ has kind ‘k’
     • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
       In an expression type signature: Proxy (b' :: c')
       In the expression: (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr
deleted file mode 100644
index bfd33693b6..0000000000
--- a/testsuite/tests/dependent/should_fail/T14066h.stderr
+++ /dev/null
@@ -1,16 +0,0 @@
-
-T14066h.hs:8:28: error:
-    • Couldn't match kind ‘* -> *’ with ‘*’
-      When matching types
-        a0 :: *
-        Maybe :: * -> *
-      Expected type: Proxy Maybe
-        Actual type: Proxy a0
-    • In the expression: fst y :: Proxy Maybe
-      In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe)
-      In an equation for ‘f’:
-          f x
-            = (fst y :: Proxy Int, fst y :: Proxy Maybe)
-            where
-                y :: (Proxy a, b)
-                y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 593b7787a1..0f7129020e 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -26,7 +26,6 @@ test('T14066d', normal, compile_fail, [''])
 test('T14066e', normal, compile_fail, [''])
 test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
-test('T14066h', normal, compile_fail, [''])
 test('T14845_fail1', normal, compile_fail, [''])
 test('T14845_fail2', normal, compile_fail, [''])
 test('InferDependency', normal, compile_fail, [''])
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index a1c412bd7d..2c1a0ec7df 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -125,10 +125,8 @@
           (Just
            [({ DumpRenamedAst.hs:9:3-36 }
              (HsIB
-              (HsIBRn
-               [{Name: a}
-               ,{Name: as}]
-               (True))
+              [{Name: a}
+              ,{Name: as}]
               (FamEqn
                (NoExt)
                ({ DumpRenamedAst.hs:9:3-8 }
@@ -183,9 +181,7 @@
                         {Name: as}))))))))))))
            ,({ DumpRenamedAst.hs:10:3-24 }
              (HsIB
-              (HsIBRn
-               []
-               (True))
+              []
               (FamEqn
                (NoExt)
                ({ DumpRenamedAst.hs:10:3-8 }
@@ -285,10 +281,8 @@
         (NoExt)
         (DataFamInstDecl
          (HsIB
-          (HsIBRn
-           [{Name: k}
-           ,{Name: a}]
-           (True))
+          [{Name: k}
+          ,{Name: a}]
           (FamEqn
            (NoExt)
            ({ DumpRenamedAst.hs:15:18-20 }
diff --git a/testsuite/tests/polykinds/T11142.stderr b/testsuite/tests/polykinds/T11142.stderr
index ea687c3247..a3b40c1222 100644
--- a/testsuite/tests/polykinds/T11142.stderr
+++ b/testsuite/tests/polykinds/T11142.stderr
@@ -1,6 +1,17 @@
 
 T11142.hs:9:49: error:
-    • Expected kind ‘k’, but ‘b’ has kind ‘k0’
+    • Expected kind ‘k1’, but ‘b’ has kind ‘k0’
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type signature:
         foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
+
+T11142.hs:10:7: error:
+    • Cannot instantiate unification variable ‘a0’
+      with a type involving foralls:
+        (forall k1 (a :: k1). SameKind a b) -> ()
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: undefined
+      In an equation for ‘foo’: foo = undefined
+    • Relevant bindings include
+        foo :: (forall k1 (a :: k1). SameKind a b) -> ()
+          (bound at T11142.hs:10:1)
diff --git a/testsuite/tests/polykinds/T11516.hs b/testsuite/tests/polykinds/T11516.hs
index 3b19a997f9..66feeec387 100644
--- a/testsuite/tests/polykinds/T11516.hs
+++ b/testsuite/tests/polykinds/T11516.hs
@@ -3,6 +3,7 @@
 {-# language ConstraintKinds #-}
 {-# language FlexibleInstances #-}
 {-# language FunctionalDependencies #-}
+{-# language UndecidableInstances #-}
 
 import GHC.Exts (Constraint)
 
diff --git a/testsuite/tests/polykinds/T11516.stderr b/testsuite/tests/polykinds/T11516.stderr
index 5db11c8f83..5f8083309c 100644
--- a/testsuite/tests/polykinds/T11516.stderr
+++ b/testsuite/tests/polykinds/T11516.stderr
@@ -1,5 +1,5 @@
 
-T11516.hs:11:16: error:
+T11516.hs:12:16: error:
     • Expected kind ‘i0 -> i0 -> *’, but ‘()’ has kind ‘*’
     • In the first argument of ‘Varpi’, namely ‘()’
       In the instance declaration for ‘Varpi (->) (->) (Either f)’
diff --git a/testsuite/tests/polykinds/T11520.hs b/testsuite/tests/polykinds/T11520.hs
index eef999d4ba..9c1d4fe1be 100644
--- a/testsuite/tests/polykinds/T11520.hs
+++ b/testsuite/tests/polykinds/T11520.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, PolyKinds, GADTs, UndecidableSuperClasses #-}
+{-# LANGUAGE RankNTypes, PolyKinds, GADTs, UndecidableSuperClasses, UndecidableInstances #-}
 
 module T11520 where
 
diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr
index 11a81baf62..75147e6a00 100644
--- a/testsuite/tests/polykinds/T11520.stderr
+++ b/testsuite/tests/polykinds/T11520.stderr
@@ -1,4 +1,8 @@
 
+T11520.hs:15:57: error:
+    • Illegal type synonym family application in instance: Compose f g
+    • In the instance declaration for ‘Typeable (Compose f g)’
+
 T11520.hs:15:77: error:
     • Expected kind ‘k20 -> k10’, but ‘g’ has kind ‘k’
     • In the second argument of ‘Compose’, namely ‘g’
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index 43f762221e..27123a8bc8 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -10,7 +10,7 @@ T12593.hs:12:31: error:
     • Expecting one more argument to ‘k’
       Expected a type, but
       ‘k’ has kind
-      ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+      ‘(((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
        -> Constraint’
     • In the kind ‘k’
       In the type signature:
@@ -22,7 +22,7 @@ T12593.hs:12:40: error:
     • Expecting two more arguments to ‘k1’
       Expected a type, but
       ‘k1’ has kind
-      ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’
+      ‘((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *’
     • In the kind ‘k1’
       In the type signature:
         run :: k2 q =>
@@ -31,13 +31,13 @@ T12593.hs:12:40: error:
 
 T12593.hs:12:47: error:
     • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-                            -> (k2 -> k3 -> *) -> *)
+                            -> (k3 -> k4 -> *) -> *)
                            -> Constraint’
                      with ‘*’
       When matching kinds
-        k2 :: *
-        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
-             -> Constraint
+        k3 :: *
+        k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
+              -> Constraint
     • In the first argument of ‘p’, namely ‘c’
       In the type signature:
         run :: k2 q =>
@@ -46,11 +46,11 @@ T12593.hs:12:47: error:
 
 T12593.hs:12:49: error:
     • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-                           -> (k2 -> k3 -> *) -> *’
+                           -> (k3 -> k4 -> *) -> *’
                      with ‘*’
       When matching kinds
-        k3 :: *
-        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k4 :: *
+        k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
     • In the second argument of ‘p’, namely ‘d’
       In the type signature:
         run :: k2 q =>
@@ -59,13 +59,13 @@ T12593.hs:12:49: error:
 
 T12593.hs:12:56: error:
     • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-                            -> (k2 -> k3 -> *) -> *)
+                            -> (k3 -> k4 -> *) -> *)
                            -> Constraint’
                      with ‘*’
       When matching kinds
         k0 :: *
-        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
-             -> Constraint
+        k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
+              -> Constraint
     • In the first argument of ‘q’, namely ‘c’
       In the type signature:
         run :: k2 q =>
@@ -74,13 +74,43 @@ T12593.hs:12:56: error:
 
 T12593.hs:12:58: error:
     • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-                           -> (k2 -> k3 -> *) -> *’
+                           -> (k3 -> k4 -> *) -> *’
                      with ‘*’
       When matching kinds
         k1 :: *
-        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
     • In the second argument of ‘q’, namely ‘d’
       In the type signature:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:14:6: error:
+    • Couldn't match type ‘Free k2 p0’ with ‘Free k6 k7 k8 p’
+      Expected type: Free k6 k7 k8 p a b
+        Actual type: Free k2 p0 a b
+    • In the pattern: Free cat
+      In an equation for ‘run’: run (Free cat) = cat
+    • Relevant bindings include
+        run :: Free k6 k7 k8 p a b
+               -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b
+          (bound at T12593.hs:14:1)
+
+T12593.hs:14:18: error:
+    • Couldn't match kind ‘*’
+                     with ‘(((k3 -> k4 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
+                           -> Constraint’
+      When matching kinds
+        k0 :: *
+        k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
+              -> Constraint
+    • In the expression: cat
+      In an equation for ‘run’: run (Free cat) = cat
+    • Relevant bindings include
+        cat :: forall (q :: k0 -> k1 -> *).
+               k2 q =>
+               (forall (c :: k0) (d :: k1). p0 c d -> q c d) -> q a b
+          (bound at T12593.hs:14:11)
+        run :: Free k6 k7 k8 p a b
+               -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b
+          (bound at T12593.hs:14:1)
diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr
deleted file mode 100644
index 3d2492e23d..0000000000
--- a/testsuite/tests/polykinds/T13555.stderr
+++ /dev/null
@@ -1,20 +0,0 @@
-
-T13555.hs:25:14: error:
-    • Couldn't match type ‘k2’ with ‘k0’
-      ‘k2’ is a rigid type variable bound by
-        the type signature for:
-          crtInfo :: forall k2 (m :: k2).
-                     Reflects m Int =>
-                     TaggedT m Maybe (CRTInfo (GF fp d))
-        at T13555.hs:25:14-79
-      Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
-        Actual type: TaggedT m0 Maybe (CRTInfo (GF fp d))
-    • When checking that instance signature for ‘crtInfo’
-        is more general than its signature in the class
-        Instance sig: forall (m :: k0).
-                      Reflects m Int =>
-                      TaggedT m Maybe (CRTInfo (GF fp d))
-           Class sig: forall k2 (m :: k2).
-                      Reflects m Int =>
-                      TaggedT m Maybe (CRTInfo (GF fp d))
-      In the instance declaration for ‘CRTrans Maybe (GF fp d)’
diff --git a/testsuite/tests/polykinds/T14520.hs b/testsuite/tests/polykinds/T14520.hs
index 23e903773b..44dc2ee18d 100644
--- a/testsuite/tests/polykinds/T14520.hs
+++ b/testsuite/tests/polykinds/T14520.hs
@@ -1,4 +1,4 @@
-{-# Language DataKinds, PolyKinds, TypeFamilies, TypeOperators #-}
+{-# Language DataKinds, PolyKinds, TypeFamilies, TypeOperators, AllowAmbiguousTypes #-}
 
 module T14520 where
 
diff --git a/testsuite/tests/polykinds/T14520.stderr b/testsuite/tests/polykinds/T14520.stderr
index e19d834b95..07042fde92 100644
--- a/testsuite/tests/polykinds/T14520.stderr
+++ b/testsuite/tests/polykinds/T14520.stderr
@@ -1,5 +1,6 @@
 
 T14520.hs:15:24: error:
-    • Expected kind ‘bat w w’, but ‘Id’ has kind ‘XXX (XXX kat0 b0) b0’
+    • Expected kind ‘bat w w’,
+        but ‘Id’ has kind ‘XXX * a0 (XXX (a0 ~>> *) a0 kat0 b0) b0’
     • In the first argument of ‘Sing’, namely ‘(Id :: bat w w)’
       In the type signature: sId :: Sing w -> Sing (Id :: bat w w)
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 3abdb88d2f..1d852031d9 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -13,10 +13,11 @@ T14846.hs:38:8: error:
                ríki a a
         at T14846.hs:38:8-48
       Expected type: ríki a a
-        Actual type: Hom riki a0 a0
+        Actual type: Hom riki a a
     • When checking that instance signature for ‘i’
         is more general than its signature in the class
-        Instance sig: forall (xx :: k0) (a :: Struct cls0).
+        Instance sig: forall k1 (cls :: k1
+                                        -> Constraint) k2 (xx :: k2) (a :: Struct cls).
                       StructI xx a =>
                       Hom riki a a
            Class sig: forall k1 (cls :: k1
@@ -31,15 +32,15 @@ T14846.hs:38:8: error:
       In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:31: error:
-    • Couldn't match kind ‘k4’ with ‘Struct cls0’
+    • Couldn't match kind ‘k4’ with ‘Struct cls2’
       ‘k4’ is a rigid type variable bound by
         the instance declaration
         at T14846.hs:37:10-65
       When matching kinds
-        cls :: k4 -> Constraint
-        cls1 :: Struct cls0 -> Constraint
-      Expected kind ‘Struct cls1’,
-        but ‘Structured a cls’ has kind ‘Struct cls’
+        cls1 :: k4 -> Constraint
+        cls0 :: Struct cls -> Constraint
+      Expected kind ‘Struct cls0’,
+        but ‘Structured a cls’ has kind ‘Struct cls1’
     • In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
       In an expression type signature: AStruct (Structured a cls)
       In the expression: struct :: AStruct (Structured a cls)
diff --git a/testsuite/tests/polykinds/T7224.stderr b/testsuite/tests/polykinds/T7224.stderr
index daab1c40a9..774a4bce69 100644
--- a/testsuite/tests/polykinds/T7224.stderr
+++ b/testsuite/tests/polykinds/T7224.stderr
@@ -2,6 +2,12 @@
 T7224.hs:6:19: error:
     • Expected kind ‘i’, but ‘i’ has kind ‘*’
     • In the first argument of ‘m’, namely ‘i’
+      In the type signature: ret' :: a -> m i i a
+      In the class declaration for ‘PMonad'’
+
+T7224.hs:7:14: error:
+    • Expected kind ‘i’, but ‘i’ has kind ‘*’
+    • In the first argument of ‘m’, namely ‘i’
       In the type signature:
-        ret' :: a -> m i i a
+        bind' :: m i j a -> (a -> m j k b) -> m i k b
       In the class declaration for ‘PMonad'’
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index 6249bf7b62..9aa4ab50d9 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -1,8 +1,14 @@
 
-T8616.hs:8:29: error:
-    • Expected a type, but ‘(Any :: k)’ has kind ‘k’
-    • In an expression type signature: (Any :: k)
-      In the expression: undefined :: (Any :: k)
+T8616.hs:8:16: error:
+    • Couldn't match kind ‘k’ with ‘*’
+      ‘k’ is a rigid type variable bound by
+        the type signature for:
+          withSomeSing :: forall k (kproxy :: k). Proxy kproxy
+        at T8616.hs:7:1-50
+      When matching types
+        a0 :: *
+        Any :: k
+    • In the expression: undefined :: (Any :: k)
       In an equation for ‘withSomeSing’:
           withSomeSing = undefined :: (Any :: k)
     • Relevant bindings include
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 425e57a946..de46acfc3a 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -161,7 +161,7 @@ test('T13394a', normal, compile, [''])
 test('T13394', normal, compile, [''])
 test('T13371', normal, compile, [''])
 test('T13393', normal, compile_fail, [''])
-test('T13555', normal, compile_fail, [''])
+test('T13555', normal, compile, [''])
 test('T13659', normal, compile_fail, [''])
 test('T13625', normal, compile_fail, [''])
 test('T13985', normal, compile_fail, [''])
@@ -176,7 +176,7 @@ test('T14450', normal, compile_fail, [''])
 test('T14172', normal, multimod_compile_fail, ['T14172.hs','-v0'])
 test('T14174', normal, compile_fail, [''])
 test('T14174a', normal, compile, [''])
-test('T14520', normal, compile_fail, [''])
+test('T14520', normal, compile_fail, ['-fprint-explicit-kinds'])
 test('T11203', normal, compile_fail, [''])
 test('T14555', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('T14563', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
diff --git a/testsuite/tests/rename/should_fail/T5951.stderr b/testsuite/tests/rename/should_fail/T5951.stderr
index 8fda353b33..a6969971ab 100644
--- a/testsuite/tests/rename/should_fail/T5951.stderr
+++ b/testsuite/tests/rename/should_fail/T5951.stderr
@@ -4,6 +4,10 @@ T5951.hs:8:8: error:
       Expected a constraint, but ‘A’ has kind ‘* -> Constraint’
     • In the instance declaration for ‘B => C’
 
+T5951.hs:8:8: error:
+    • Instance head is not headed by a class: C
+    • In the instance declaration for ‘B => C’
+
 T5951.hs:9:8: error:
     • Expecting one more argument to ‘B’
       Expected a constraint, but ‘B’ has kind ‘* -> Constraint’
diff --git a/testsuite/tests/rename/should_fail/rnfail026.hs b/testsuite/tests/rename/should_fail/rnfail026.hs
index d09d9fc22f..2d22df20d4 100644
--- a/testsuite/tests/rename/should_fail/rnfail026.hs
+++ b/testsuite/tests/rename/should_fail/rnfail026.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE RankNTypes, FlexibleInstances #-}
 
--- This one made ghc-4.08 crash 
+-- This one made ghc-4.08 crash
 -- rename/RnEnv.lhs:239: Non-exhaustive patterns in function get_tycon_key
 -- The type in the Monad instance is utterly bogus, of course
 
@@ -9,11 +9,12 @@ module ShouldCompile ( Set ) where
 
 data Set a = Set [a]
        deriving (Eq, Ord, Read, Show)
-
+{-
 instance Functor Set where
         f `fmap` (Set xs) = Set $ f `fmap` xs
-
+-}
 instance Monad (forall a. Eq a => Set a) where
         return x = Set [x]
-
-instance Eq (forall a. [a]) where 
+{-
+instance Eq (forall a. [a]) where
+-}
diff --git a/testsuite/tests/rename/should_fail/rnfail026.stderr b/testsuite/tests/rename/should_fail/rnfail026.stderr
index 8bd80b1b58..79b07c4d24 100644
--- a/testsuite/tests/rename/should_fail/rnfail026.stderr
+++ b/testsuite/tests/rename/should_fail/rnfail026.stderr
@@ -1,10 +1,10 @@
 
+rnfail026.hs:16:10: error:
+    • Illegal polymorphic type: forall a. Eq a => Set a
+    • In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
+
 rnfail026.hs:16:27: error:
     • Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’
     • In the first argument of ‘Monad’, namely
         ‘(forall a. Eq a => Set a)’
       In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
-
-rnfail026.hs:19:10: error:
-    • Illegal polymorphic type: forall a. [a]
-    • In the instance declaration for ‘Eq (forall a. [a])’
diff --git a/testsuite/tests/th/T5358.stderr b/testsuite/tests/th/T5358.stderr
index b698bc1004..4bfc53a78e 100644
--- a/testsuite/tests/th/T5358.stderr
+++ b/testsuite/tests/th/T5358.stderr
@@ -1,24 +1,4 @@
 
-T5358.hs:10:13: error:
-    • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
-    • The function ‘T5358.t1’ is applied to one argument,
-      but its type ‘Int’ has none
-      In the first argument of ‘(==)’, namely ‘T5358.t1 x’
-      In the expression: T5358.t1 x == T5358.t2 x
-    • Relevant bindings include
-        x :: t (bound at T5358.hs:10:9)
-        T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
-
-T5358.hs:10:21: error:
-    • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
-    • The function ‘T5358.t2’ is applied to one argument,
-      but its type ‘Int’ has none
-      In the second argument of ‘(==)’, namely ‘T5358.t2 x’
-      In the expression: T5358.t1 x == T5358.t2 x
-    • Relevant bindings include
-        x :: t (bound at T5358.hs:10:9)
-        T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
-
 T5358.hs:14:12: error:
     • Exception when trying to run compile-time code:
         runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool
diff --git a/testsuite/tests/typecheck/should_compile/T15141.hs b/testsuite/tests/typecheck/should_compile/T15141.hs
new file mode 100644
index 0000000000..c0cb5d8488
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15141.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE PolyKinds, TypeFamilies, TypeFamilyDependencies,
+             ScopedTypeVariables, TypeOperators, GADTs,
+             DataKinds #-}
+
+module T15141 where
+
+import Data.Type.Equality
+import Data.Proxy
+
+type family F a = r | r -> a where
+  F () = Bool
+
+data Wumpus where
+  Unify :: k1 ~ F k2 => k1 -> k2 -> Wumpus
+
+f :: forall k (a :: k). k :~: Bool -> ()
+f Refl = let x :: Proxy ('Unify a b)
+             x = undefined
+         in ()
+
+{-
+We want this situation:
+
+forall[1] k[1].
+  [G] k ~ Bool
+  forall [2] ... . [W] k ~ F kappa[2]
+
+where the inner wanted can be solved only by taking the outer
+given into account. This means that the wanted needs to be floated out.
+More germane to this bug, we need *not* to generalize over kappa.
+
+The code above builds this scenario fairly exactly, and indeed fails
+without the logic in kindGeneralize that excludes constrained variables
+from generalization.
+-}
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 2fb5429715..1857ba814e 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -646,3 +646,4 @@ test('T15431', normal, compile, [''])
 test('T15431a', normal, compile, [''])
 test('T15428', normal, compile, [''])
 test('T15412', normal, compile, [''])
+test('T15141', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T11112.stderr b/testsuite/tests/typecheck/should_fail/T11112.stderr
index ec2154c8ce..304078158e 100644
--- a/testsuite/tests/typecheck/should_fail/T11112.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11112.stderr
@@ -1,5 +1,13 @@
 
 T11112.hs:3:9: error:
     • Expected a type, but ‘Ord s’ has kind ‘Constraint’
-    • In the type signature:
-        sort :: Ord s -> [s] -> [s]
+    • In the type signature: sort :: Ord s -> [s] -> [s]
+
+T11112.hs:4:11: error:
+    • Couldn't match expected type ‘[s] -> [s]’
+                  with actual type ‘Ord s’
+    • In the expression: xs
+      In an equation for ‘sort’: sort xs = xs
+    • Relevant bindings include
+        xs :: Ord s (bound at T11112.hs:4:6)
+        sort :: Ord s => [s] -> [s] (bound at T11112.hs:4:1)
diff --git a/testsuite/tests/typecheck/should_fail/T11563.stderr b/testsuite/tests/typecheck/should_fail/T11563.stderr
index 27eca84816..1283c33983 100644
--- a/testsuite/tests/typecheck/should_fail/T11563.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11563.stderr
@@ -1,4 +1,10 @@
 
+T11563.hs:5:10: error:
+    • Variable ‘s’ occurs more often
+        in the constraint ‘C s’ than in the instance head ‘C T’
+      (Use UndecidableInstances to permit this)
+    • In the instance declaration for ‘C T’
+
 T11563.hs:5:19: error:
     • Expecting one more argument to ‘T’
       Expected a type, but ‘T’ has kind ‘* -> *’
diff --git a/testsuite/tests/typecheck/should_fail/T14232.stderr b/testsuite/tests/typecheck/should_fail/T14232.stderr
index a497be7b19..1ca41f0bd5 100644
--- a/testsuite/tests/typecheck/should_fail/T14232.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14232.stderr
@@ -2,3 +2,16 @@
 T14232.hs:3:6: error:
     • Expected kind ‘* -> *’, but ‘String -> a’ has kind ‘*’
     • In the type signature: f :: (String -> a) String -> a
+
+T14232.hs:4:9: error:
+    • Couldn't match type ‘String -> a’ with ‘(->) t0’
+      Expected type: t0 -> [Char]
+        Actual type: (String -> a) String
+    • The function ‘g’ is applied to one argument,
+      but its type ‘(String -> a) String’ has none
+      In the expression: g s
+      In an equation for ‘f’: f g s = g s
+    • Relevant bindings include
+        s :: t0 (bound at T14232.hs:4:5)
+        g :: (String -> a) String (bound at T14232.hs:4:3)
+        f :: (String -> a) String -> a (bound at T14232.hs:4:1)
diff --git a/testsuite/tests/typecheck/should_fail/T1633.stderr b/testsuite/tests/typecheck/should_fail/T1633.stderr
index 300e6c3def..5d9dcc44f5 100644
--- a/testsuite/tests/typecheck/should_fail/T1633.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1633.stderr
@@ -1,5 +1,5 @@
 
 T1633.hs:8:18: error:
-    Expected kind ‘* -> *’, but ‘Bool’ has kind ‘*’
-    In the first argument of ‘Functor’, namely ‘Bool’
-    In the instance declaration for ‘Functor Bool’
+    • Expected kind ‘* -> *’, but ‘Bool’ has kind ‘*’
+    • In the first argument of ‘Functor’, namely ‘Bool’
+      In the instance declaration for ‘Functor Bool’
diff --git a/testsuite/tests/typecheck/should_fail/T2994.stderr b/testsuite/tests/typecheck/should_fail/T2994.stderr
index 7f20acf5aa..09b36165a6 100644
--- a/testsuite/tests/typecheck/should_fail/T2994.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2994.stderr
@@ -5,12 +5,20 @@ T2994.hs:11:10: error:
         but ‘MonadReader Int’ has kind ‘* -> Constraint’
     • In the instance declaration for ‘MonadReader Int’
 
+T2994.hs:11:10: error:
+    • Instance head is not headed by a class: MonadReader Int
+    • In the instance declaration for ‘MonadReader Int’
+
 T2994.hs:13:10: error:
     • Expecting one more argument to ‘MonadReader (Reader' r)’
       Expected a constraint,
         but ‘MonadReader (Reader' r)’ has kind ‘* -> Constraint’
     • In the instance declaration for ‘MonadReader (Reader' r)’
 
+T2994.hs:13:10: error:
+    • Instance head is not headed by a class: MonadReader (Reader' r)
+    • In the instance declaration for ‘MonadReader (Reader' r)’
+
 T2994.hs:13:23: error:
     • Expecting one more argument to ‘Reader' r’
       Expected a type, but ‘Reader' r’ has kind ‘* -> *’
@@ -21,3 +29,8 @@ T2994.hs:15:10: error:
     • Expected kind ‘(* -> *) -> Constraint’,
         but ‘MonadReader r r’ has kind ‘Constraint’
     • In the instance declaration for ‘MonadReader r r (Reader' r)’
+
+T2994.hs:15:10: error:
+    • Instance head is not headed by a class:
+        MonadReader r r (Reader' r)
+    • In the instance declaration for ‘MonadReader r r (Reader' r)’
diff --git a/testsuite/tests/typecheck/should_fail/T3540.stderr b/testsuite/tests/typecheck/should_fail/T3540.stderr
index 0fdb88b313..eeb2c051f2 100644
--- a/testsuite/tests/typecheck/should_fail/T3540.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3540.stderr
@@ -3,6 +3,16 @@ T3540.hs:4:12: error:
     • Expected a type, but ‘a ~ Int’ has kind ‘Constraint’
     • In the type signature: thing :: (a ~ Int)
 
+T3540.hs:5:9: error:
+    • Couldn't match kind ‘Constraint’ with ‘*’
+      When matching types
+        a0 :: *
+        a ~ Int :: Constraint
+    • In the expression: undefined
+      In an equation for ‘thing’: thing = undefined
+    • Relevant bindings include
+        thing :: a ~ Int (bound at T3540.hs:5:1)
+
 T3540.hs:7:20: error:
     • Expected a type, but ‘a ~ Int’ has kind ‘Constraint’
     • In the type signature: thing1 :: Int -> (a ~ Int)
diff --git a/testsuite/tests/typecheck/should_fail/T7778.stderr b/testsuite/tests/typecheck/should_fail/T7778.stderr
index a0f10fcd92..1993b772e0 100644
--- a/testsuite/tests/typecheck/should_fail/T7778.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7778.stderr
@@ -1,4 +1,10 @@
 
+T7778.hs:3:6: error:
+    • Illegal qualified type: Num Int => Num
+      A constraint must be a monotype
+      Perhaps you intended to use QuantifiedConstraints
+    • In the type signature: v :: ((Num Int => Num) ()) => ()
+
 T7778.hs:3:7: error:
     • Expected kind ‘* -> Constraint’,
         but ‘Num Int => Num’ has kind ‘*’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail057.stderr b/testsuite/tests/typecheck/should_fail/tcfail057.stderr
index 945c81c1cd..9ddffeb28b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail057.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail057.stderr
@@ -1,5 +1,13 @@
 
 tcfail057.hs:5:7: error:
     • Expected a type, but ‘RealFrac a’ has kind ‘Constraint’
-    • In the type signature:
-        f :: (RealFrac a) -> a -> a
+    • In the type signature: f :: (RealFrac a) -> a -> a
+
+tcfail057.hs:6:7: error:
+    • Couldn't match expected type ‘a -> a’
+                  with actual type ‘RealFrac a’
+    • In the expression: x
+      In an equation for ‘f’: f x = x
+    • Relevant bindings include
+        x :: RealFrac a (bound at tcfail057.hs:6:3)
+        f :: RealFrac a => a -> a (bound at tcfail057.hs:6:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail058.stderr b/testsuite/tests/typecheck/should_fail/tcfail058.stderr
index 478aa7f467..5150637cb9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail058.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail058.stderr
@@ -2,5 +2,24 @@
 tcfail058.hs:6:7: error:
     • Expecting one more argument to ‘Array a’
       Expected a constraint, but ‘Array a’ has kind ‘* -> *’
-    • In the type signature:
-        f :: (Array a) => a -> b
+    • In the type signature: f :: (Array a) => a -> b
+
+tcfail058.hs:7:7: error:
+    • Could not deduce: a ~ b
+      from the context: Array a
+        bound by the type signature for:
+                   f :: forall a b. Array a => a -> b
+        at tcfail058.hs:6:1-24
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. Array a => a -> b
+        at tcfail058.hs:6:1-24
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. Array a => a -> b
+        at tcfail058.hs:6:1-24
+    • In the expression: x
+      In an equation for ‘f’: f x = x
+    • Relevant bindings include
+        x :: a (bound at tcfail058.hs:7:3)
+        f :: a -> b (bound at tcfail058.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail063.stderr b/testsuite/tests/typecheck/should_fail/tcfail063.stderr
index 935390e436..7dd1e9ce02 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail063.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail063.stderr
@@ -2,5 +2,21 @@
 tcfail063.hs:6:9: error:
     • Expecting one more argument to ‘Num’
       Expected a constraint, but ‘Num’ has kind ‘* -> Constraint’
-    • In the type signature:
-        moby :: Num => Int -> a -> Int
+    • In the type signature: moby :: Num => Int -> a -> Int
+
+tcfail063.hs:7:14: error:
+    • Could not deduce: a ~ Int
+      from the context: Num
+        bound by the type signature for:
+                   moby :: forall a. Num => Int -> a -> Int
+        at tcfail063.hs:6:1-30
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          moby :: forall a. Num => Int -> a -> Int
+        at tcfail063.hs:6:1-30
+    • In the second argument of ‘(+)’, namely ‘y’
+      In the expression: x + y
+      In an equation for ‘moby’: moby x y = x + y
+    • Relevant bindings include
+        y :: a (bound at tcfail063.hs:7:8)
+        moby :: Int -> a -> Int (bound at tcfail063.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail078.stderr b/testsuite/tests/typecheck/should_fail/tcfail078.stderr
index 014d589bf6..a0816a746c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail078.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail078.stderr
@@ -2,3 +2,16 @@
 tcfail078.hs:5:6: error:
     • Expected kind ‘* -> Constraint’, but ‘Integer’ has kind ‘*’
     • In the type signature: f :: Integer i => i
+
+tcfail078.hs:6:19: error:
+    • Could not deduce (Num i) arising from the literal ‘0’
+      from the context: Integer i
+        bound by the type signature for:
+                   f :: forall i. Integer i => i
+        at tcfail078.hs:5:1-19
+      Possible fix:
+        add (Num i) to the context of
+          the type signature for:
+            f :: forall i. Integer i => i
+    • In the expression: 0
+      In an equation for ‘f’: f = 0
diff --git a/testsuite/tests/typecheck/should_fail/tcfail113.stderr b/testsuite/tests/typecheck/should_fail/tcfail113.stderr
index fbdffa5ab9..80c97d2737 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail113.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail113.stderr
@@ -4,11 +4,32 @@ tcfail113.hs:12:7: error:
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
     • In the type signature: f :: [Maybe]
 
+tcfail113.hs:13:1: error:
+    • Couldn't match expected type ‘[Maybe]’
+                  with actual type ‘p1 -> p1’
+    • The equation(s) for ‘f’ have one argument,
+      but its type ‘[Maybe]’ has none
+    • Relevant bindings include
+        f :: [Maybe] (bound at tcfail113.hs:13:1)
+
 tcfail113.hs:15:8: error:
     • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the first argument of ‘T’, namely ‘Int’
       In the type signature: g :: T Int
 
+tcfail113.hs:16:1: error:
+    • Couldn't match expected type ‘T Int’ with actual type ‘p0 -> p0’
+    • The equation(s) for ‘g’ have one argument,
+      but its type ‘T Int’ has none
+    • Relevant bindings include g :: T Int (bound at tcfail113.hs:16:1)
+
 tcfail113.hs:18:6: error:
     • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the type signature: h :: Int Int
+
+tcfail113.hs:19:1: error:
+    • Couldn't match type ‘Int’ with ‘(->) Int’
+      Expected type: Int Int
+        Actual type: Int -> Int
+    • The equation(s) for ‘h’ have one argument,
+      but its type ‘Int Int’ has none
diff --git a/testsuite/tests/typecheck/should_fail/tcfail158.stderr b/testsuite/tests/typecheck/should_fail/tcfail158.stderr
index 12f8a4e8df..995be74380 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail158.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail158.stderr
@@ -1,6 +1,3 @@
 
-tcfail158.hs:14:19: error:
-    • Expecting one more argument to ‘Val v’
-      Expected a type, but ‘Val v’ has kind ‘* -> *’
-    • In the type signature:
-        bar :: forall v. Val v
+tcfail158.hs:1:1: error:
+    The IO action ‘main’ is not defined in module ‘Main’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail160.stderr b/testsuite/tests/typecheck/should_fail/tcfail160.stderr
index 46a7640cf9..400b2bf5a4 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail160.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail160.stderr
@@ -2,5 +2,10 @@
 tcfail160.hs:7:8: error:
     • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the first argument of ‘T’, namely ‘Int’
-      In the type signature:
-        g :: T Int
+      In the type signature: g :: T Int
+
+tcfail160.hs:8:1: error:
+    • Couldn't match expected type ‘T Int’ with actual type ‘p0 -> p0’
+    • The equation(s) for ‘g’ have one argument,
+      but its type ‘T Int’ has none
+    • Relevant bindings include g :: T Int (bound at tcfail160.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail161.stderr b/testsuite/tests/typecheck/should_fail/tcfail161.stderr
index ce783bb5ab..89042d1d20 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail161.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail161.stderr
@@ -2,5 +2,12 @@
 tcfail161.hs:5:7: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    • In the type signature:
-        f :: [Maybe]
+    • In the type signature: f :: [Maybe]
+
+tcfail161.hs:6:1: error:
+    • Couldn't match expected type ‘[Maybe]’
+                  with actual type ‘p0 -> p0’
+    • The equation(s) for ‘f’ have one argument,
+      but its type ‘[Maybe]’ has none
+    • Relevant bindings include
+        f :: [Maybe] (bound at tcfail161.hs:6:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail212.stderr b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
index 8eb7e6e57f..8ceab3e931 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail212.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
@@ -2,21 +2,31 @@
 tcfail212.hs:10:7: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    • In the type signature:
-        f :: (Maybe, Either Int)
+    • In the type signature: f :: (Maybe, Either Int)
 
 tcfail212.hs:10:14: error:
     • Expecting one more argument to ‘Either Int’
       Expected a type, but ‘Either Int’ has kind ‘* -> *’
-    • In the type signature:
-        f :: (Maybe, Either Int)
+    • In the type signature: f :: (Maybe, Either Int)
+
+tcfail212.hs:11:6: error:
+    • Couldn't match expected type ‘Maybe’
+                  with actual type ‘Maybe Integer’
+    • In the expression: Just 1
+      In the expression: (Just 1, Left 1)
+      In an equation for ‘f’: f = (Just 1, Left 1)
+
+tcfail212.hs:11:14: error:
+    • Couldn't match expected type ‘Either Int’
+                  with actual type ‘Either Integer b0’
+    • In the expression: Left 1
+      In the expression: (Just 1, Left 1)
+      In an equation for ‘f’: f = (Just 1, Left 1)
 
 tcfail212.hs:13:7: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
-    • In the type signature:
-        g :: (Int#, Int#)
+    • In the type signature: g :: (Int#, Int#)
 
 tcfail212.hs:13:13: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
-    • In the type signature:
-        g :: (Int#, Int#)
+    • In the type signature: g :: (Int#, Int#)
diff --git a/utils/haddock b/utils/haddock
-Subproject 612f44f9a582b1f7c8a9ba709651bce83692b60
+Subproject a264b6b3e41dd42946110afcf5000341e5fb3a6