Be more careful about quantification

This MR is driven by #23051. It does several things:

* It is guided by the generalisation plan described in #20686.
  But it is still far from a complete implementation of that plan.

* Add Note [Inferred type with escaping kind] to GHC.Tc.Gen.Bind.
  This explains that we don't (yet, pending #20686) directly
  prevent generalising over escaping kinds.

* In `GHC.Tc.Utils.TcMType.defaultTyVar` we default RuntimeRep
  and Multiplicity variables, beause we don't want to quantify over
  them.  We want to do the same for a Concrete tyvar, but there is
  nothing sensible to default it to (unless it has kind RuntimeRep,
  in which case it'll be caught by an earlier case). So we promote
  instead.

* Pure refactoring in GHC.Tc.Solver:
  * Rename decideMonoTyVars to decidePromotedTyVars, since that's
    what it does.

  * Move the actual promotion of the tyvars-to-promote from
    `defaultTyVarsAndSimplify` to `decidePromotedTyVars`.  This is a
    no-op; just tidies up the code.  E.g then we don't need to
    return the promoted tyvars from `decidePromotedTyVars`.

  * A little refactoring in `defaultTyVarsAndSimplify`, but no
    change in behaviour.

* When making a TauTv unification variable into a ConcreteTv
  (in GHC.Tc.Utils.Concrete.makeTypeConcrete), preserve the occ-name
  of the type variable.  This just improves error messages.

* Kill off dead code: GHC.Tc.Utils.TcMType.newConcreteHole

7 files changed, 215 insertions, 160 deletions

diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index c957fc7fcd..1e9a25c63d 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -903,15 +903,19 @@ mkInferredPolyId residual insoluble qtvs inferred_theta poly_name mb_sig_inst mo
        ; let inferred_poly_ty = mkInvisForAllTys binders (mkPhiTy theta' mono_ty')
 
        ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta'
-                                          , ppr inferred_poly_ty])
+                                          , ppr inferred_poly_ty
+                                          , text "insoluble" <+> ppr insoluble ])
+
        ; unless insoluble $
          addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
          do { checkEscapingKind inferred_poly_ty
+                 -- See Note [Inferred type with escaping kind]
             ; checkValidType (InfSigCtxt poly_name) inferred_poly_ty }
-         -- See Note [Validity of inferred types]
-         -- If we found an insoluble error in the function definition, don't
-         -- do this check; otherwise (#14000) we may report an ambiguity
-         -- error for a rather bogus type.
+                 -- See Note [Validity of inferred types]
+         -- unless insoluble: if we found an insoluble error in the
+         -- function definition, don't do this check; otherwise
+         -- (#14000) we may report an ambiguity error for a rather
+         -- bogus type.
 
        ; return (mkLocalId poly_name ManyTy inferred_poly_ty) }
 
@@ -1176,6 +1180,33 @@ Examples that might fail:
                                 or multi-parameter type classes
  - an inferred type that includes unboxed tuples
 
+Note [Inferred type with escaping kind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Check for an inferred type with an escaping kind; e.g. #23051
+   forall {k} {f :: k -> RuntimeRep} {g :: k} {a :: TYPE (f g)}. a
+where the kind of the body of the forall mentions `f` and `g` which
+are bound by the forall.  No no no.
+
+This check, mkInferredPolyId, is really in the wrong place:
+`inferred_poly_ty` doesn't obey the PKTI and it would be better not to
+generalise it in the first place; see #20686.  But for now it works.
+
+How else could we avoid generalising over escaping type variables? I
+considered:
+
+* Adjust the generalisation in GHC.Tc.Solver to directly check for
+  escaping kind variables; instead, promote or default them. But that
+  gets into the defaulting swamp and is a non-trivial and unforced
+  change, so I have left it alone for now.
+
+* When inferring the type of a binding, in `tcMonoBinds`, we create
+  an ExpSigmaType with `tcInfer`.  If we simply gave it an ir_frr field
+  that said "must have fixed runtime rep", then the kind would be made
+  Concrete; and we never generalise over Concrete variables.  A bit
+  more indirect, but we need the "don't generalise over Concrete variables"
+  stuff anyway.
+
+
 Note [Impedance matching]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 374567ce69..c002d8cc3e 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2037,7 +2037,7 @@ typecheck/should_compile/tc170).
 Moreover in instance heads we get forall-types with
 kind Constraint.
 
-It's tempting to check that the body kind is either * or #. But this is
+It's tempting to check that the body kind is (TYPE _). But this is
 wrong. For example:
 
   class C a b
@@ -2046,7 +2046,7 @@ wrong. For example:
 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
-convenient. Bottom line: don't check for * or # here.
+convenient. Bottom line: don't check for (TYPE _) here.
 
 Note [Body kind of a HsQualTy]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3547,8 +3547,12 @@ kindGeneralizeSome skol_info wanted kind_or_type
          -- here will already have all type variables quantified;
          -- thus, every free variable is really a kv, never a tv.
        ; dvs <- candidateQTyVarsOfKind kind_or_type
-       ; dvs <- filterConstrainedCandidates wanted dvs
-       ; quantifyTyVars skol_info DefaultNonStandardTyVars dvs }
+       ; filtered_dvs <- filterConstrainedCandidates wanted dvs
+       ; traceTc "kindGeneralizeSome" $
+         vcat [ text "type:" <+> ppr kind_or_type
+              , text "dvs:" <+> ppr dvs
+              , text "filtered_dvs:" <+> ppr filtered_dvs ]
+       ; quantifyTyVars skol_info DefaultNonStandardTyVars filtered_dvs }
 
 filterConstrainedCandidates
   :: WantedConstraints    -- Don't quantify over variables free in these
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index fad6cbae4f..b46b994e2f 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1279,10 +1279,6 @@ emitResidualConstraints rhs_tclvl ev_binds_var
     -- uniformly.
 
 --------------------
-ctsPreds :: Cts -> [PredType]
-ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
-                             , let ev = ctEvidence ct ]
-
 findInferredDiff :: TcThetaType -> TcThetaType -> TcM TcThetaType
 -- Given a partial type signature f :: (C a, D a, _) => blah
 -- and the inferred constraints (X a, D a, Y a, C a)
@@ -1397,7 +1393,7 @@ Note [Deciding quantification]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If the monomorphism restriction does not apply, then we quantify as follows:
 
-* Step 1: decideMonoTyVars.
+* Step 1: decidePromotedTyVars.
   Take the global tyvars, and "grow" them using functional dependencies
      E.g.  if x:alpha is in the environment, and alpha ~ [beta] (which can
           happen because alpha is untouchable here) then do not quantify over
@@ -1408,10 +1404,11 @@ If the monomorphism restriction does not apply, then we quantify as follows:
   We also account for the monomorphism restriction; if it applies,
   add the free vars of all the constraints.
 
-  Result is mono_tvs; we will not quantify over these.
+  Result is mono_tvs; we will promote all of these to the outer levek,
+  and certainly not quantify over them.
 
 * Step 2: defaultTyVarsAndSimplify.
-  Default any non-mono tyvars (i.e ones that are definitely
+  Default any non-promoted tyvars (i.e ones that are definitely
   not going to become further constrained), and re-simplify the
   candidate constraints.
 
@@ -1431,7 +1428,7 @@ If the monomorphism restriction does not apply, then we quantify as follows:
   over are determined in Step 3 (not in Step 1), it is OK for
   the mono_tvs to be missing some variables free in the
   environment. This is why removing the psig_qtvs is OK in
-  decideMonoTyVars. Test case for this scenario: T14479.
+  decidePromotedTyVars. Test case for this scenario: T14479.
 
 * Step 3: decideQuantifiedTyVars.
   Decide which variables to quantify over, as follows:
@@ -1559,7 +1556,7 @@ and we are running simplifyInfer over
 
 These are two implication constraints, both of which contain a
 wanted for the class C. Neither constraint mentions the bound
-skolem. We might imagine that these constraint could thus float
+skolem. We might imagine that these constraints could thus float
 out of their implications and then interact, causing beta1 to unify
 with beta2, but constraints do not currently float out of implications.
 
@@ -1609,12 +1606,12 @@ decideQuantification
 -- See Note [Deciding quantification]
 decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
   = do { -- Step 1: find the mono_tvs
-       ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode
-                                              name_taus psigs candidates
+       ; (candidates, co_vars) <- decidePromotedTyVars infer_mode
+                                        name_taus psigs candidates
 
        -- Step 2: default any non-mono tyvars, and re-simplify
        -- This step may do some unification, but result candidates is zonked
-       ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
+       ; candidates <- defaultTyVarsAndSimplify rhs_tclvl candidates
 
        -- Step 3: decide which kind/type variables to quantify over
        ; qtvs <- decideQuantifiedTyVars skol_info name_taus psigs candidates
@@ -1647,7 +1644,6 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
            (vcat [ text "infer_mode:" <+> ppr infer_mode
                  , text "candidates:" <+> ppr candidates
                  , text "psig_theta:" <+> ppr psig_theta
-                 , text "mono_tvs:"   <+> ppr mono_tvs
                  , text "co_vars:"    <+> ppr co_vars
                  , text "qtvs:"       <+> ppr qtvs
                  , text "theta:"      <+> ppr theta ])
@@ -1686,23 +1682,34 @@ ambiguous types.  Something like
 But that's a battle for another day.
 -}
 
-decideMonoTyVars :: InferMode
-                 -> [(Name,TcType)]
-                 -> [TcIdSigInst]
-                 -> [PredType]
-                 -> TcM (TcTyCoVarSet, [PredType], CoVarSet)
--- Decide which tyvars and covars cannot be generalised:
---   (a) Free in the environment
---   (b) Mentioned in a constraint we can't generalise
---   (c) Connected by an equality or fundep to (a) or (b)
+decidePromotedTyVars :: InferMode
+                     -> [(Name,TcType)]
+                     -> [TcIdSigInst]
+                     -> [PredType]
+                     -> TcM ([PredType], CoVarSet)
+-- We are about to generalise over type variables at level N
+-- Each must be either
+--    (P) promoted
+--    (D) defaulted
+--    (Q) quantified
+-- This function finds (P), the type variables that we are going to promote:
+--   (a) Mentioned in a constraint we can't generalise (the MR)
+--   (b) Mentioned in the kind of a CoVar; we can't quantify over a CoVar,
+--       so we must not quantify over a type variable free in its kind
+--   (c) Connected by an equality or fundep to
+--          * a type variable at level < N, or
+--          * A tyvar subject to (a), (b) or (c)
+-- Having found all such level-N tyvars that we can't generalise,
+-- promote them, to eliminate them from further consideration.
+--
 -- Also return CoVars that appear free in the final quantified types
 --   we can't quantify over these, and we must make sure they are in scope
-decideMonoTyVars infer_mode name_taus psigs candidates
+decidePromotedTyVars infer_mode name_taus psigs candidates
   = do { (no_quant, maybe_quant) <- pick infer_mode candidates
 
        -- If possible, we quantify over partial-sig qtvs, so they are
        -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs
-       ; psig_qtvs <-  zonkTcTyVarsToTcTyVars $ binderVars $
+       ; psig_qtvs <- zonkTcTyVarsToTcTyVars $ binderVars $
                       concatMap (map snd . sig_inst_skols) psigs
 
        ; psig_theta <- mapM TcM.zonkTcType $
@@ -1713,29 +1720,31 @@ decideMonoTyVars infer_mode name_taus psigs candidates
        ; tc_lvl <- TcM.getTcLevel
        ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
 
+             -- (b) The co_var_tvs are tvs mentioned in the types of covars or
+             -- coercion holes. We can't quantify over these covars, so we
+             -- must include the variable in their types in the mono_tvs.
+             -- E.g.  If we can't quantify over co :: k~Type, then we can't
+             --       quantify over k either!  Hence closeOverKinds
+             -- Recall that coVarsOfTypes also returns coercion holes
              co_vars = coVarsOfTypes (psig_tys ++ taus ++ candidates)
              co_var_tvs = closeOverKinds co_vars
-               -- The co_var_tvs are tvs mentioned in the types of covars or
-               -- coercion holes. We can't quantify over these covars, so we
-               -- must include the variable in their types in the mono_tvs.
-               -- E.g.  If we can't quantify over co :: k~Type, then we can't
-               --       quantify over k either!  Hence closeOverKinds
 
              mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
                          tyCoVarsOfTypes candidates
                -- We need to grab all the non-quantifiable tyvars in the
                -- types so that we can grow this set to find other
-               -- non-quantifiable tyvars. This can happen with something
-               -- like
+               -- non-quantifiable tyvars. This can happen with something like
                --    f x y = ...
                --      where z = x 3
                -- The body of z tries to unify the type of x (call it alpha[1])
                -- with (beta[2] -> gamma[2]). This unification fails because
-               -- alpha is untouchable. But we need to know not to quantify over
-               -- beta or gamma, because they are in the equality constraint with
-               -- alpha. Actual test case: typecheck/should_compile/tc213
+               -- alpha is untouchable, leaving [W] alpha[1] ~ (beta[2] -> gamma[2]).
+               -- We need to know not to quantify over beta or gamma, because they
+               -- are in the equality constraint with alpha. Actual test case:
+               -- typecheck/should_compile/tc213
 
              mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
+
                -- mono_tvs1 is now the set of variables from an outer scope
                -- (that's mono_tvs0) and the set of covars, closed over kinds.
                -- Given this set of variables we know we will not quantify,
@@ -1749,9 +1758,8 @@ decideMonoTyVars infer_mode name_taus psigs candidates
                -- (that is, we might have IP "c" Bool and IP "c" Int in different
                -- places within the same program), and
                -- skipping this causes implicit params to monomorphise too many
-               -- variables; see Note [Inheriting implicit parameters] in
-               -- GHC.Tc.Solver. Skipping causes typecheck/should_compile/tc219
-               -- to fail.
+               -- variables; see Note [Inheriting implicit parameters] in GHC.Tc.Solver.
+               -- Skipping causes typecheck/should_compile/tc219 to fail.
 
              mono_tvs2 = closeWrtFunDeps non_ip_candidates mono_tvs1
                -- mono_tvs2 now contains any variable determined by the "root
@@ -1761,7 +1769,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
                                closeWrtFunDeps non_ip_candidates (tyCoVarsOfTypes no_quant)
                                 `minusVarSet` mono_tvs2
              -- constrained_tvs: the tyvars that we are not going to
-             -- quantify solely because of the monomorphism restriction
+             -- quantify /solely/ because of the monomorphism restriction
              --
              -- (`minusVarSet` mono_tvs2): a type variable is only
              --   "constrained" (so that the MR bites) if it is not
@@ -1783,7 +1791,12 @@ decideMonoTyVars infer_mode name_taus psigs candidates
            let dia = TcRnMonomorphicBindings (map fst name_taus)
            diagnosticTc (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus) dia
 
-       ; traceTc "decideMonoTyVars" $ vcat
+       -- Promote the mono_tvs
+       -- See Note [Promote monomorphic tyvars]
+       ; traceTc "decidePromotedTyVars: promotion:" (ppr mono_tvs)
+       ; _ <- promoteTyVarSet mono_tvs
+
+       ; traceTc "decidePromotedTyVars" $ vcat
            [ text "infer_mode =" <+> ppr infer_mode
            , text "mono_tvs0 =" <+> ppr mono_tvs0
            , text "no_quant =" <+> ppr no_quant
@@ -1791,7 +1804,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
            , text "mono_tvs =" <+> ppr mono_tvs
            , text "co_vars =" <+> ppr co_vars ]
 
-       ; return (mono_tvs, maybe_quant, co_vars) }
+       ; return (maybe_quant, co_vars) }
   where
     pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
     -- Split the candidates into ones we definitely
@@ -1811,48 +1824,34 @@ decideMonoTyVars infer_mode name_taus psigs candidates
 
 -------------------
 defaultTyVarsAndSimplify :: TcLevel
-                         -> TyCoVarSet          -- Promote these mono-tyvars
                          -> [PredType]          -- Assumed zonked
                          -> TcM [PredType]      -- Guaranteed zonked
--- Promote the known-monomorphic tyvars;
 -- Default any tyvar free in the constraints;
 -- and re-simplify in case the defaulting allows further simplification
-defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
-  = do {  -- Promote any tyvars that we cannot generalise
-          -- See Note [Promote monomorphic tyvars]
-       ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
-       ; _ <- promoteTyVarSet mono_tvs
-
-       -- Default any kind/levity vars
+defaultTyVarsAndSimplify rhs_tclvl candidates
+  = do {  -- Default any kind/levity vars
        ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
                 <- candidateQTyVarsOfTypes candidates
-                -- any covars should already be handled by
-                -- the logic in decideMonoTyVars, which looks at
-                -- the constraints generated
+         -- NB1: decidePromotedTyVars has promoted any type variable fixed by the
+         --      type envt, so they won't be chosen by candidateQTyVarsOfTypes
+         -- NB2: Defaulting for variables free in tau_tys is done later, by quantifyTyVars
+         --      Hence looking only at 'candidates'
+         -- NB3: Any covars should already be handled by
+         --      the logic in decidePromotedTyVars, which looks at
+         --      the constraints generated
 
        ; poly_kinds  <- xoptM LangExt.PolyKinds
-       ; mapM_ (default_one poly_kinds True) (dVarSetElems cand_kvs)
-       ; mapM_ (default_one poly_kinds False) (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
+       ; let default_kv | poly_kinds = default_tv
+                        | otherwise  = defaultTyVar DefaultKindVars
+             default_tv = defaultTyVar (NonStandardDefaulting DefaultNonStandardTyVars)
+       ; mapM_ default_kv (dVarSetElems cand_kvs)
+       ; mapM_ default_tv (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
 
        ; simplify_cand candidates
        }
   where
-    default_one poly_kinds is_kind_var tv
-      | not (isMetaTyVar tv)
-      = return ()
-      | tv `elemVarSet` mono_tvs
-      = return ()
-      | otherwise
-      = void $ defaultTyVar
-          (if not poly_kinds && is_kind_var
-           then DefaultKindVars
-           else NonStandardDefaulting DefaultNonStandardTyVars)
-          -- NB: only pass 'DefaultKindVars' when we know we're dealing with a kind variable.
-          tv
-
-       -- this common case (no inferred constraints) should be fast
-    simplify_cand [] = return []
-       -- see Note [Unconditionally resimplify constraints when quantifying]
+    -- See Note [Unconditionally resimplify constraints when quantifying]
+    simplify_cand [] = return []  -- Fast path
     simplify_cand candidates
       = do { clone_wanteds <- newWanteds DefaultOrigin candidates
            ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $
@@ -2086,7 +2085,7 @@ sure to quantify over them.  This leads to several wrinkles:
 
   In the signature for 'g', we cannot quantify over 'b' because it turns out to
   get unified with 'a', which is free in g's environment.  So we carefully
-  refrain from bogusly quantifying, in GHC.Tc.Solver.decideMonoTyVars.  We
+  refrain from bogusly quantifying, in GHC.Tc.Solver.decidePromotedTyVars.  We
   report the error later, in GHC.Tc.Gen.Bind.chooseInferredQuantifiers.
 
 Note [growThetaTyVars vs closeWrtFunDeps]
@@ -2122,7 +2121,7 @@ constraint (transitively).
 
 We use closeWrtFunDeps in places where we need to know which variables are
 *always* determined by some seed set. This includes
-  * when determining the mono-tyvars in decideMonoTyVars. If `a`
+  * when determining the mono-tyvars in decidePromotedTyVars. If `a`
     is going to be monomorphic, we need b and c to be also: they
     are determined by the choice for `a`.
   * when checking instance coverage, in
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index d10c4394f6..7d4911263f 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -15,7 +15,7 @@ module GHC.Tc.Types.Constraint (
         assertFuelPrecondition, assertFuelPreconditionStrict,
         emptyCts, andCts, andManyCts, pprCts,
         singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
-        isEmptyCts,
+        isEmptyCts, ctsPreds,
         isPendingScDict, pendingScDict_maybe,
         superClassesMightHelp, getPendingWantedScs,
         isWantedCt, isGivenCt,
@@ -1043,6 +1043,9 @@ emptyCts = emptyBag
 isEmptyCts :: Cts -> Bool
 isEmptyCts = isEmptyBag
 
+ctsPreds :: Cts -> [PredType]
+ctsPreds cts = foldr ((:) . ctPred) [] cts
+
 pprCts :: Cts -> SDoc
 pprCts cts = vcat (map ppr (bagToList cts))
 
diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs
index 95f2a026a7..d69a3c473a 100644
--- a/compiler/GHC/Tc/Utils/Concrete.hs
+++ b/compiler/GHC/Tc/Utils/Concrete.hs
@@ -37,8 +37,12 @@ import GHC.Tc.Utils.TcMType    ( newConcreteTyVar, isFilledMetaTyVar_maybe, writ
                                , emitWantedEq )
 
 import GHC.Types.Basic         ( TypeOrKind(..) )
+import GHC.Types.Name          ( getOccName )
+import GHC.Types.Name.Occurrence( occNameFS )
 import GHC.Utils.Misc          ( HasDebugCallStack )
 import GHC.Utils.Outputable
+import GHC.Data.FastString     ( fsLit )
+
 
 import Control.Monad      ( void )
 import Data.Functor       ( ($>) )
@@ -495,7 +499,7 @@ unifyConcrete frr_orig ty
            -- Create a new ConcreteTv metavariable @concrete_tv@
            -- and unify @ty ~# concrete_tv@.
          ; _  ->
-    do { conc_tv <- newConcreteTyVar (ConcreteFRR frr_orig) ki
+    do { conc_tv <- newConcreteTyVar (ConcreteFRR frr_orig) (fsLit "cx") ki
            -- NB: newConcreteTyVar asserts that 'ki' is concrete.
        ; coToMCo <$> emitWantedEq orig KindLevel Nominal ty (mkTyVarTy conc_tv) } } }
   where
@@ -647,9 +651,12 @@ makeTypeConcrete conc_orig ty =
                , TauTv <- metaTyVarInfo tv
                -> -- Change the MetaInfo to ConcreteTv, but retain the TcLevel
                do { kind <- go (tyVarKind tv)
+                  ; let occ_fs = occNameFS (getOccName tv)
+                        -- occ_fs: preserve the occurrence name of the original tyvar
+                        -- This helps in error messages
                   ; lift $
                     do { conc_tv <- setTcLevel (tcTyVarLevel tv) $
-                                    newConcreteTyVar conc_orig kind
+                                    newConcreteTyVar conc_orig occ_fs kind
                        ; let conc_ty = mkTyVarTy conc_tv
                        ; writeMetaTyVar tv conc_ty
                        ; return conc_ty } }
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index d0afe71560..9536f58a58 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -45,8 +45,6 @@ module GHC.Tc.Utils.TcMType (
   unpackCoercionHole, unpackCoercionHole_maybe,
   checkCoercionHole,
 
-  ConcreteHole, newConcreteHole,
-
   newImplication,
 
   --------------------------------
@@ -414,23 +412,6 @@ checkCoercionHole cv co
              | otherwise
              = False
 
--- | A coercion hole used to store evidence for `Concrete#` constraints.
---
--- See Note [The Concrete mechanism].
-type ConcreteHole = CoercionHole
-
--- | Create a new (initially unfilled) coercion hole,
--- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint.
-newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy')
-                -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep')
-                -> TcM (ConcreteHole, TcType)
-                  -- ^ where to put the evidence, and a metavariable to store
-                  -- the concrete type
-newConcreteHole ki ty
-  = do { concrete_ty <- newFlexiTyVarTy ki
-       ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty
-       ; hole <- newCoercionHole co_ty
-       ; return (hole, concrete_ty) }
 
 {- **********************************************************************
 *
@@ -840,11 +821,13 @@ cloneTyVarTyVar name kind
 --
 -- Invariant: the kind must be concrete, as per Note [ConcreteTv].
 -- This is checked with an assertion.
-newConcreteTyVar :: HasDebugCallStack => ConcreteTvOrigin -> TcKind -> TcM TcTyVar
-newConcreteTyVar reason kind =
-  assertPpr (isConcrete kind)
-    (text "newConcreteTyVar: non-concrete kind" <+> ppr kind)
-  $ newAnonMetaTyVar (ConcreteTv reason) kind
+newConcreteTyVar :: HasDebugCallStack => ConcreteTvOrigin
+                 -> FastString -> TcKind -> TcM TcTyVar
+newConcreteTyVar reason fs kind
+  = assertPpr (isConcrete kind) assert_msg $
+    newNamedAnonMetaTyVar fs (ConcreteTv reason) kind
+  where
+    assert_msg = text "newConcreteTyVar: non-concrete kind" <+> ppr kind
 
 newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
 newPatSigTyVar name kind
@@ -1242,14 +1225,14 @@ NB: this is all rather similar to, but sadly not the same as
 
 Wrinkle:
 
-We must make absolutely sure that alpha indeed is not
-from an outer context. (Otherwise, we might indeed learn more information
-about it.) This can be done easily: we just check alpha's TcLevel.
-That level must be strictly greater than the ambient TcLevel in order
-to treat it as naughty. We say "strictly greater than" because the call to
+We must make absolutely sure that alpha indeed is not from an outer
+context. (Otherwise, we might indeed learn more information about it.)
+This can be done easily: we just check alpha's TcLevel.  That level
+must be strictly greater than the ambient TcLevel in order to treat it
+as naughty. We say "strictly greater than" because the call to
 candidateQTyVars is made outside the bumped TcLevel, as stated in the
-comment to candidateQTyVarsOfType. The level check is done in go_tv
-in collect_cand_qtvs. Skipping this check caused #16517.
+comment to candidateQTyVarsOfType. The level check is done in go_tv in
+collect_cand_qtvs. Skipping this check caused #16517.
 
 -}
 
@@ -1349,8 +1332,9 @@ candidateQTyVarsWithBinders :: [TyVar] -> Type -> TcM CandidatesQTvs
 -- Because we are going to scoped-sort the quantified variables
 -- in among the tvs
 candidateQTyVarsWithBinders bound_tvs ty
-  = do { kvs <- candidateQTyVarsOfKinds (map tyVarKind bound_tvs)
-       ; all_tvs <- collect_cand_qtvs ty False emptyVarSet kvs ty
+  = do { kvs     <- candidateQTyVarsOfKinds (map tyVarKind bound_tvs)
+       ; cur_lvl <- getTcLevel
+       ; all_tvs <- collect_cand_qtvs ty False cur_lvl emptyVarSet kvs ty
        ; return (all_tvs `delCandidates` bound_tvs) }
 
 -- | Gathers free variables to use as quantification candidates (in
@@ -1362,14 +1346,18 @@ candidateQTyVarsWithBinders bound_tvs ty
 -- See Note [Dependent type variables]
 candidateQTyVarsOfType :: TcType       -- not necessarily zonked
                        -> TcM CandidatesQTvs
-candidateQTyVarsOfType ty = collect_cand_qtvs ty False emptyVarSet mempty ty
+candidateQTyVarsOfType ty
+  = do { cur_lvl <- getTcLevel
+       ; collect_cand_qtvs ty False cur_lvl emptyVarSet mempty ty }
 
 -- | Like 'candidateQTyVarsOfType', but over a list of types
 -- The variables to quantify must have a TcLevel strictly greater than
 -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
 candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
-candidateQTyVarsOfTypes tys = foldlM (\acc ty -> collect_cand_qtvs ty False emptyVarSet acc ty)
-                                     mempty tys
+candidateQTyVarsOfTypes tys
+  = do { cur_lvl <- getTcLevel
+       ; foldlM (\acc ty -> collect_cand_qtvs ty False cur_lvl emptyVarSet acc ty)
+                mempty tys }
 
 -- | Like 'candidateQTyVarsOfType', but consider every free variable
 -- to be dependent. This is appropriate when generalizing a *kind*,
@@ -1377,16 +1365,21 @@ candidateQTyVarsOfTypes tys = foldlM (\acc ty -> collect_cand_qtvs ty False empt
 -- to Type.)
 candidateQTyVarsOfKind :: TcKind       -- Not necessarily zonked
                        -> TcM CandidatesQTvs
-candidateQTyVarsOfKind ty = collect_cand_qtvs ty True emptyVarSet mempty ty
+candidateQTyVarsOfKind ty
+  = do { cur_lvl <- getTcLevel
+       ; collect_cand_qtvs ty True cur_lvl emptyVarSet mempty ty }
 
 candidateQTyVarsOfKinds :: [TcKind]    -- Not necessarily zonked
                        -> TcM CandidatesQTvs
-candidateQTyVarsOfKinds tys = foldM (\acc ty -> collect_cand_qtvs ty True emptyVarSet acc ty)
-                                    mempty tys
+candidateQTyVarsOfKinds tys
+  = do { cur_lvl <- getTcLevel
+       ; foldM (\acc ty -> collect_cand_qtvs ty True cur_lvl emptyVarSet acc ty)
+               mempty tys }
 
 collect_cand_qtvs
-  :: TcType          -- original type that we started recurring into; for errors
+  :: TcType          -- Original type that we started recurring into; for errors
   -> Bool            -- True <=> consider every fv in Type to be dependent
+  -> TcLevel         -- Current TcLevel; collect only tyvars whose level is greater
   -> VarSet          -- Bound variables (locals only)
   -> CandidatesQTvs  -- Accumulating parameter
   -> Type            -- Not necessarily zonked
@@ -1403,7 +1396,7 @@ collect_cand_qtvs
 --     so that subsequent dependency analysis (to build a well
 --     scoped telescope) works correctly
 
-collect_cand_qtvs orig_ty is_dep bound dvs ty
+collect_cand_qtvs orig_ty is_dep cur_lvl bound dvs ty
   = go dvs ty
   where
     is_bound tv = tv `elemVarSet` bound
@@ -1411,13 +1404,13 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
     -----------------
     go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs
     -- Uses accumulating-parameter style
-    go dv (AppTy t1 t2)    = foldlM go dv [t1, t2]
-    go dv (TyConApp tc tys) = go_tc_args dv (tyConBinders tc) tys
+    go dv (AppTy t1 t2)       = foldlM go dv [t1, t2]
+    go dv (TyConApp tc tys)   = go_tc_args dv (tyConBinders tc) tys
     go dv (FunTy _ w arg res) = foldlM go dv [w, arg, res]
-    go dv (LitTy {})        = return dv
-    go dv (CastTy ty co)    = do dv1 <- go dv ty
-                                 collect_cand_qtvs_co orig_ty bound dv1 co
-    go dv (CoercionTy co)   = collect_cand_qtvs_co orig_ty bound dv co
+    go dv (LitTy {})          = return dv
+    go dv (CastTy ty co)      = do { dv1 <- go dv ty
+                                   ; collect_cand_qtvs_co orig_ty cur_lvl bound dv1 co }
+    go dv (CoercionTy co)     = collect_cand_qtvs_co orig_ty cur_lvl bound dv co
 
     go dv (TyVarTy tv)
       | is_bound tv = return dv
@@ -1427,8 +1420,8 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
                              Nothing     -> go_tv dv tv }
 
     go dv (ForAllTy (Bndr tv _) ty)
-      = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv)
-           ; collect_cand_qtvs orig_ty is_dep (bound `extendVarSet` tv) dv1 ty }
+      = do { dv1 <- collect_cand_qtvs orig_ty True cur_lvl bound dv (tyVarKind tv)
+           ; collect_cand_qtvs orig_ty is_dep cur_lvl (bound `extendVarSet` tv) dv1 ty }
 
       -- This makes sure that we default e.g. the alpha in Proxy alpha (Any alpha).
       -- Tested in polykinds/NestedProxies.
@@ -1437,7 +1430,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
       -- to look at kinds.
     go_tc_args dv (tc_bndr:tc_bndrs) (ty:tys)
       = do { dv1 <- collect_cand_qtvs orig_ty (is_dep || isNamedTyConBinder tc_bndr)
-                                      bound dv ty
+                                      cur_lvl bound dv ty
            ; go_tc_args dv1 tc_bndrs tys }
     go_tc_args dv _bndrs tys  -- _bndrs might be non-empty: undersaturation
                               -- tys might be non-empty: oversaturation
@@ -1446,6 +1439,21 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
 
     -----------------
     go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
+      | tcTyVarLevel tv <= cur_lvl
+      = return dv   -- This variable is from an outer context; skip
+                    -- See Note [Use level numbers for quantification]
+
+      | case tcTyVarDetails tv of
+          SkolemTv _ lvl _ -> lvl > pushTcLevel cur_lvl
+          _                -> False
+      = return dv  -- Skip inner skolems
+        -- This only happens for erroneous program with bad telescopes
+        -- e.g. BadTelescope2:  forall a k (b :: k). SameKind a b
+        --      We have (a::k), and at the outer we don't want to quantify
+        --      over the already-quantified skolem k.
+        -- (Apparently we /do/ want to quantify over skolems whose level sk_lvl is
+        -- sk_lvl > cur_lvl; you get lots of failures otherwise. A battle for another day.)
+
       | tv `elemDVarSet` kvs
       = return dv  -- We have met this tyvar already
 
@@ -1461,17 +1469,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
                  -- (which comes next) works correctly
 
            ; let tv_kind_vars = tyCoVarsOfType tv_kind
-           ; cur_lvl <- getTcLevel
-           ; if |  tcTyVarLevel tv <= cur_lvl
-                -> return dv   -- this variable is from an outer context; skip
-                               -- See Note [Use level numbers for quantification]
-
-                | case tcTyVarDetails tv of
-                     SkolemTv _ lvl _ -> lvl > pushTcLevel cur_lvl
-                     _                -> False
-                -> return dv  -- Skip inner skolems; ToDo: explain
-
-                |  intersectsVarSet bound tv_kind_vars
+           ; if | intersectsVarSet bound tv_kind_vars
                    -- the tyvar must not be from an outer context, but we have
                    -- already checked for this.
                    -- See Note [Naughty quantification candidates]
@@ -1490,25 +1488,26 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
                                 -- See Note [Order of accumulation]
 
                         -- See Note [Recurring into kinds for candidateQTyVars]
-                      ; collect_cand_qtvs orig_ty True bound dv' tv_kind } }
+                      ; collect_cand_qtvs orig_ty True cur_lvl bound dv' tv_kind } }
 
 collect_cand_qtvs_co :: TcType -- original type at top of recursion; for errors
+                     -> TcLevel
                      -> VarSet -- bound variables
                      -> CandidatesQTvs -> Coercion
                      -> TcM CandidatesQTvs
-collect_cand_qtvs_co orig_ty bound = go_co
+collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
   where
-    go_co dv (Refl ty)               = collect_cand_qtvs orig_ty True bound dv ty
-    go_co dv (GRefl _ ty mco)        = do dv1 <- collect_cand_qtvs orig_ty True bound dv ty
-                                          go_mco dv1 mco
+    go_co dv (Refl ty)               = collect_cand_qtvs orig_ty True cur_lvl bound dv ty
+    go_co dv (GRefl _ ty mco)        = do { dv1 <- collect_cand_qtvs orig_ty True cur_lvl bound dv ty
+                                          ; go_mco dv1 mco }
     go_co dv (TyConAppCo _ _ cos)    = foldlM go_co dv cos
     go_co dv (AppCo co1 co2)         = foldlM go_co dv [co1, co2]
     go_co dv (FunCo _ _ _ w co1 co2) = foldlM go_co dv [w, co1, co2]
     go_co dv (AxiomInstCo _ _ cos)   = foldlM go_co dv cos
     go_co dv (AxiomRuleCo _ cos)     = foldlM go_co dv cos
-    go_co dv (UnivCo prov _ t1 t2)   = do dv1 <- go_prov dv prov
-                                          dv2 <- collect_cand_qtvs orig_ty True bound dv1 t1
-                                          collect_cand_qtvs orig_ty True bound dv2 t2
+    go_co dv (UnivCo prov _ t1 t2)   = do { dv1 <- go_prov dv prov
+                                          ; dv2 <- collect_cand_qtvs orig_ty True cur_lvl bound dv1 t1
+                                          ; collect_cand_qtvs orig_ty True cur_lvl bound dv2 t2 }
     go_co dv (SymCo co)              = go_co dv co
     go_co dv (TransCo co1 co2)       = foldlM go_co dv [co1, co2]
     go_co dv (SelCo _ co)            = go_co dv co
@@ -1527,7 +1526,7 @@ collect_cand_qtvs_co orig_ty bound = go_co
 
     go_co dv (ForAllCo tcv kind_co co)
       = do { dv1 <- go_co dv kind_co
-           ; collect_cand_qtvs_co orig_ty (bound `extendVarSet` tcv) dv1 co }
+           ; collect_cand_qtvs_co orig_ty cur_lvl (bound `extendVarSet` tcv) dv1 co }
 
     go_mco dv MRefl    = return dv
     go_mco dv (MCo co) = go_co dv co
@@ -1543,7 +1542,7 @@ collect_cand_qtvs_co orig_ty bound = go_co
       | cv `elemVarSet` cvs = return dv
 
         -- See Note [Recurring into kinds for candidateQTyVars]
-      | otherwise           = collect_cand_qtvs orig_ty True bound
+      | otherwise           = collect_cand_qtvs orig_ty True cur_lvl bound
                                     (dv { dv_cvs = cvs `extendVarSet` cv })
                                     (idType cv)
 
@@ -1810,17 +1809,30 @@ defaultTyVar def_strat tv
   = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
        ; writeMetaTyVar tv liftedRepTy
        ; return True }
+
   | isLevityVar tv
   , default_ns_vars
   = do { traceTc "Defaulting a Levity var to Lifted" (ppr tv)
        ; writeMetaTyVar tv liftedDataConTy
        ; return True }
+
   | isMultiplicityVar tv
   , default_ns_vars
   = do { traceTc "Defaulting a Multiplicity var to Many" (ppr tv)
        ; writeMetaTyVar tv manyDataConTy
        ; return True }
 
+  | isConcreteTyVar tv
+    -- We don't want to quantify; but neither can we default to
+    -- anything sensible.  (If it has kind RuntimeRep or Levity, as is
+    -- often the case, it'll have been caught earlier by earlier
+    -- cases. So in this exotic situation we just promote.  Not very
+    -- satisfing, but it's very much a corner case: #23051
+    -- We should really implement the plan in #20686.
+  = do { lvl <- getTcLevel
+       ; _ <- promoteMetaTyVarTo lvl tv
+       ; return True }
+
   | DefaultKindVars <- def_strat -- -XNoPolyKinds and this is a kind var: we must default it
   = default_kind_var tv
 
@@ -1872,9 +1884,8 @@ defaultTyVars ns_strat dvs
        ; let
            def_tvs, def_kvs :: DefaultingStrategy
            def_tvs = NonStandardDefaulting ns_strat
-           def_kvs
-             | poly_kinds = def_tvs
-             | otherwise  = DefaultKindVars
+           def_kvs | poly_kinds = def_tvs
+                   | otherwise  = DefaultKindVars
              -- As -XNoPolyKinds precludes polymorphic kind variables, we default them.
              -- For example:
              --
@@ -1965,7 +1976,7 @@ What do do?
  D. We could error.
 
 We choose (D), as described in #17567, and implement this choice in
-doNotQuantifyTyVars.  Discussion of alternativs A-C is below.
+doNotQuantifyTyVars.  Discussion of alternatives A-C is below.
 
 NB: this is all rather similar to, but sadly not the same as
     Note [Naughty quantification candidates]
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index f088a7e6ab..d9df4913bc 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -475,7 +475,7 @@ This is not OK: we get
   MkT :: forall l. T @l :: TYPE (BoxedRep l)
 which is ill-kinded.
 
-For ordinary /user-written type signatures f :: blah, we make this
+For ordinary /user-written/ type signatures f :: blah, we make this
 check as part of kind-checking the type signature in tcHsSigType; see
 Note [Escaping kind in type signatures] in GHC.Tc.Gen.HsType.