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

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.

Start with the minimal conv in reproducer and investigate how pattern matching interacts with the @[congr] lemma sum_congr, especially the reported unknown metavariable. Done means the expression is matched and simplified correctly, or the command produces a meaningful error instead of the RPC failure; retest against the Lean nightly version.