Apparent violation of TcLevel invariant in T7173

This is T7173:

showEnv' env t = se 10 env t
 where
   se p env (Bind n b sc) = sb env n b
   sb env n t             = se 10 env t

data TT n = Bind n (TT n) (TT n)

In GHC.Tc.Solver.decideQuantification, if I collect all metavariables and inspect their TcLevels, say with a patch like the following

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index e9d59946d3..20326f4f63 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1689,7 +1689,7 @@ decideQuantification
 decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
   = do { -- Step 1: find the mono_tvs
        ; (candidates, co_vars, mono_tvs0)
-             <- decidePromotedTyVars infer_mode name_taus psigs candidates
+             <- decidePromotedTyVars infer_mode rhs_tclvl 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
@@ -1797,6 +1797,7 @@ Some rationale and observations
 -}

 decidePromotedTyVars :: InferMode
+                     -> TcLevel
                      -> [(Name,TcType)]
                      -> [TcIdSigInst]
                      -> [PredType]
@@ -1818,7 +1819,7 @@ decidePromotedTyVars :: InferMode
 --
 -- 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
-decidePromotedTyVars infer_mode name_taus psigs candidates
+decidePromotedTyVars infer_mode rhs_tclvl name_taus psigs candidates
   = do { tc_lvl <- TcM.getTcLevel
        ; (no_quant, maybe_quant) <- pick infer_mode candidates

@@ -1833,7 +1834,18 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
              ; return (psig_qtvs, psig_theta, taus) }

        ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
-
+             all_tvs = tyCoVarsOfTypesList (psig_tys ++ candidates ++ taus)
+
+        ; let bad_tvs = filter (\ tv -> isMetaTyVar tv && metaTyVarTcLevel tv `strictlyDeeperThan` rhs_tclvl) all_tvs
+        ; forM_ bad_tvs $ \ bad_tv ->
+            do { tv_contents <- TcM.readTcRef (metaTyVarRef bad_tv)
+               ; pprTraceM "decideQuantification: bad_tv" $
+                    vcat [ text "curr_tclvl:" <+> ppr tc_lvl
+                         , text "rhs_tclvl:" <+> ppr rhs_tclvl
+                         , text "bad_tv:" <+> ppr bad_tv
+                         , text "contents:" <+> ppr tv_contents ] }
+
+       ; let
              -- (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.

then we find that, when processing the outer showEnv' binding after having handled the recursive group {se, sb}, we see a metavariable that violates the TcLevel invariant:

decideQuantification: bad_tv
  curr_tclvl: 0
  rhs_tclvl: 1
  bad_tv: p_aBU[tau:2]
  contents: Flexi

That is, we're at TcLevel 1 but we encounter a metavariable with level 2!

It's perhaps a bit clearer to use named wildcards (with a patch like !10170 to be able to see the user-written variable names):

showEnv' :: _env2 -> TT _n -> _res
showEnv' env t = se 10 env t
 where
   se :: Num _bad => _bad -> _env -> TT _n -> _res
   se p env (Bind n b sc) = sb env n b

   sb :: _env -> _n -> TT _n -> _res
   sb env n t             = se 10 env t

decideQuantification: bad_tv
  curr_tclvl: 0
  rhs_tclvl: 1
  bad_tv: _bad_aBL[tau:2]
  contents: Flexi

Note that, for some reason, if I change the metavariable _env2 to _env, then the problem goes away.

I came across this while attempting to implement the defaulting plan in #20686. @simonpj @rae