`conv in` can unexpectedly fail with `unknown metavariable` error

[vlad902]

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

conv in pat is supposed to pattern match on the pattern pat. The following reproducer below fails unexpectedly with a unknown metavariable '?_uniq.301' error. The following minimized reproducer shows that the failure has to do with a lemma with a @congr annotation.

Context

This issue was minimized from this Zulip discussion.

Steps to Reproduce

def sum (_ : Nat → Nat) : Nat := 0

@[congr]
theorem sum_congr {f g} : (∀ x, f x = g x) → sum f = sum g := by sorry

theorem repro : (sum fun i ↦ sum fun j : Nat ↦ i + 1) = 0 := by
  conv in (fun j : Nat ↦ _ + 1) => simp
  sorry

Expected behavior: conv in correctly matches the sub-expression, or at the very least fails with a meaningful error message.

Actual behavior: Fails with an RPC error, unknown metavariable '?_uniq.301'

Versions

Lean 4.28.0-nightly-2026-01-02
Target: x86_64-unknown-linux-gnu

(Taken from lean-live)

Impact

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

[plp127]

I spent an afternoon debugging this yesterday and identified the problem.

conv in pat => tacs is short for conv => pattern pat; tacs, and pattern uses simp:

lean4/src/Lean/Elab/Tactic/Conv/Pattern.lean

Line 132 in 3804a1d

let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state })

simp then tries the congr lemma using trySimpCongrTheorem?, which increments the metavariable context depth:

lean4/src/Lean/Meta/Tactic/Simp/Main.lean

Line 925 in fab1897

def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do withParent e do

Eventually, simp is called again recursively, and execution goes back to the pattern code, which find the pattern and creates metavariables in this higher metavariable context depth, which are smuggled out of the simp call using a IO.Ref PatternMatchState:

lean4/src/Lean/Elab/Tactic/Conv/Pattern.lean

Lines 91 to 92 in 3804a1d

	let (rhs, newGoal) ← mkConvGoalFor e
	state.modify (·.accept newGoal.mvarId!)

Then after the recursive calls are done, trySimpCongrTheorem? fails anyways because the proof that the rewritten goal equals the original goal contains metavariables:

lean4/src/Lean/Meta/Tactic/Simp/Main.lean

Lines 969 to 971 in fab1897

	if (← hasAssignableMVar proof <||> hasAssignableMVar eNew) then
	trace[Meta.Tactic.simp.congr] "{c.theoremName} has unassigned metavariables"
	return none

It leaves the new metavariable context depth, which invalidates any new metavariables created within in that depth.
Finally, the pattern code replaces the goal with these now invalid metavariables:

lean4/src/Lean/Elab/Tactic/Conv/Pattern.lean

Line 143 in 3804a1d

replaceMainGoal subgoals.toList

We get a "unknown metavariable" error.

[nomeata]

Thanks for the analysis. So the summary is that conv uses the simp machinery in a way that the simp API is probably not meant to be used, smuggling data out using IO.Ref?