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.

16 files changed, 235 insertions, 226 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