bug: metavariable context being rolled back in simp

This seems to be the underlying cause of leanprover-community/mathlib4#15785 and leanprover-community/aesop#153 . Unfortunately, since it involves the metaprogramming API to simp, it is difficult to give a small reproduction. The example below uses a minimalistic simp wrapper which uses a pre method to replace occurrences of G α with Nat.zero. Importantly, while doing so it creates and instantiates a universe metavariable, and something in the main simp loop seems to forget that it is instantiated, presumably rolling back the metavariable context while still holding on to the expressions generated in that context, leading to panics and unsolved metavariables in the resulting proofs.

import Lean

axiom F (s : Nat) (f : Nat → Nat) : Nat
@[congr] axiom F_congr {s₁ s₂ : Nat} {f : Nat → Nat} (h : s₁ = s₂) : F s₁ f = F s₂ f
axiom G.{u} : Sort u → Nat
axiom G_zero (α) : G α = Nat.zero

theorem foo : F (G True) (fun x => x) ≤ F (G True) id := by
  open Lean Meta Elab Tactic in run_tac
    let g ← getMainGoal
    let ctx := {
      simpTheorems := #[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}]
      congrTheorems := ← getSimpCongrTheorems }
    let pre e := do
      if e.isAppOfArity ``G 1 then
        let u ← mkFreshLevelMVar
        let α := e.appArg!
        guard <| ← isDefEq (← inferType α) (.sort u)
        let pf := Expr.app (.const ``G_zero [u]) α
        -- let pf ← instantiateMVars pf
        logInfo <| repr pf
        logInfo pf
        pure <| .done { expr := .const ``Nat.zero [], proof? := pf }
      else
        pure .continue
    let tgt ← g.getType
    let (res, _) ← Simp.main tgt ctx (methods := { pre })
    logInfo res.proof?
    replaceMainGoal [← applySimpResultToTarget g tgt res]
  apply Nat.le_refl

-- invalid occurrence of universe level 'u_1' at 'foo', it does not occur at the declaration type,
-- nor it is explicit universe level provided by the user, occurring at expression
--   G.{u_1} True
-- at declaration body
--   Eq.mpr (id (congr (congrArg LE.le (F_congr (G_zero True))) (congrArg (fun (x : Nat) ↦ F x id) (G_zero True))))
--     (Nat.le_refl (F Nat.zero fun (x : Nat) ↦ x))

Run the embedded Lean reproduction and inspect the custom pre method, Simp.main, and applySimpResultToTarget flow. Trace how the universe metavariable created by mkFreshLevelMVar is handled during simplification. Done means the example no longer panics or produces unsolved metavariables or an invalid universe level.