`Meta.check` Fails After `revert`

Prerequisites

• 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

This is an issue with delayed assigned metavariables. In the context of a metavariable, if the target type contains another metavariable, and some free variable gets reverted, Meta.check fails.

Context

https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/.60Meta.2Echeck.60.20fails.20after.20revert/with/563285554

Steps to Reproduce

1. Execute the following snippet either in LSP or lean --run

import Lean
open Lean

#eval do
  let statement ← instantiateMVars $ ← Elab.Term.elabTerm (← `(term|forall (n m: Nat) (h: n = m), n.succ = m.succ)) .none
  Meta.forallTelescope statement λ _fvars target => do
  let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
  let u ← Meta.mkFreshLevelMVar
  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
  let f ← Meta.mkFreshExprSyntheticOpaqueMVar (.forallE .anonymous α β .default)
  let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
  let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
  let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
  let fvars := (← h.mvarId!.getDecl).lctx.foldl (init := []) λ acc decl => acc ++ [decl.fvarId]
  let (_, h') ← h.mvarId!.revert #[fvars[2]!] true
  h'.withContext do
    Meta.check (← h'.getType)

Expected behavior:

Meta.check succeeds, so nothing gets printed.

Actual behavior:

Mystery.lean:4:0: error: Application type mismatch: The argument
  ?m.5
has type
  ?m.3
but is expected to have type
  ?m.3
in the application
  Eq ?m.5

Note that the two ?m.3 are different. Set pp.all true to see.

Versions

Lean (version 4.28.0-nightly-2026-01-12, x86_64-unknown-linux-gnu, commit e56351da7ae15673a5bc2b83e7fb70e1fbd988ca, Release)

Also occurs on 4.27.0

on Arch Linux

Also happens in Lean v4.26.0

Additional Information

This is related to #5279

Impact

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

Start with the self-contained Lean snippet in the issue and run it using lean --run or in LSP. Investigate the interaction between delayed assigned metavariables, Meta.forallTelescope, revert, and Meta.check, with related issue #5279 as context. Done means the reproduction succeeds without the application type mismatch.