`MVarId.revert` assigns mvars in the wrong direction

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The function MVarId.revert should not be assigning mvars other than its argument, but I found a case where this happens. Consider this example, where ?{lhs,rhs} are .natural:

| n : Nat
?snd : Eq Prop ?lhs ?rhs
| n : Nat
?lhs : Prop
| n : Nat
?rhs : Prop

and if I now execute revert on ?snd (reverting n), I get

?snd : forall (n: Nat), Eq Nat ?lhs' ?rhs'

with the side effect of assigning ?lhs, ?rhs. This is suppressed when these mvars are .syntheticOpaque.

Context

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Collect.20mvars.20during.20a.20tactic/near/468311815

Steps to Reproduce

This example:

import Lean
open Lean

def showMVar (name: String) (mvarId: MVarId): MetaM Unit := mvarId.withContext do
  if let .some expr ← getExprMVarAssignment? mvarId then
    IO.println s!"{name} := {← Meta.ppExpr expr}"
  else if let .some a ← getDelayedMVarAssignment? mvarId then
    IO.println s!"{name} ::= {← Meta.ppExpr $ .mvar a.mvarIdPending}"
  else
    IO.println s!"{name} is not assigned"

def metaM: MetaM Unit := do
  let α: Expr := .sort 0
  let nat: Expr := .const `Nat []
  Meta.withLocalDecl `x .default nat $ λ fvar => do
    let lhs: Expr ← Meta.mkFreshExprMVar (type? := .some α) (userName := `lhs)
    let rhs ← Meta.mkFreshExprSyntheticOpaqueMVar α `rhs
    let goalType ← Meta.mkEq lhs rhs
    let goal ← Meta.mkFreshExprSyntheticOpaqueMVar goalType
    IO.println s!"goal: {← Meta.ppExpr $ ← goal.mvarId!.getType}"
    let (_, goal2) ← goal.mvarId!.revert #[fvar.fvarId!]
    goal2.withContext do
      IO.println s!"goal2 : {← Meta.ppExpr $ ← goal2.getType}"
    let .forallE _ _ body _ ← goal2.getType | panic! "This must be a ∀"
    let .some (_, .app lhs' (.bvar _), .app rhs' (.bvar _)) := body.eq? | panic! "Wrong type"
    showMVar "lhs" lhs.mvarId!
    showMVar "rhs" rhs.mvarId!
    showMVar "lhs'" lhs'.mvarId!
    showMVar "rhs'" rhs'.mvarId!

def main : IO Unit := do
  let env: Environment ← importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
  let options: Options := {}
  let options := options.setBool `pp.all true
  let coreM := Meta.MetaM.run' metaM
  let coreContext: Lean.Core.Context := {
    options,
    currNamespace := `Example
    openDecls := [],     -- No 'open' directives needed
    fileName := "<stdin>",
    fileMap := { source := "", positions := #[0] }
  }
  match ← (coreM.run' coreContext { env }).toBaseIO with
  | .error exception =>
    IO.println s!"{← exception.toMessageData.toString}"
  | .ok _ => return ()

Expected behavior:: ?lhs, ?rhs do not get assigned. Whatever mvar revert generates gets delayed assigned to ?lhs, ?rhs

Actual behavior:: ?lhs got assigned. ?rhs was not assigned and the generated mvar (?rhs') is correctly delayed assigned to ?rhs. This is IMO correct behaviour.

Versions

This happens on 4.10.0-rc1 and nightly-2024-09-06.

Additional Information

Meta.withNewMCtxDepth causes mvar not found errors, so it can't be used as a workaround.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal Lean program in the issue and run it against the reported versions to reproduce the assignment of ?lhs. Read MVarId.revert and the Meta.withNewMCtxDepth context mentioned in the report. Done means reverting the mvar does not assign unrelated mvars, while generated mvars are delayed-assigned as expected.