Metavariable introduced in pattern match

[math-fehr]

Description

When doing nested pattern matching, some function arguments built using (by ...) become metavariables in other terms that are being matched.

def Rewriter.createOpTest (ctx: Nat) (a: Option Nat) (h : pred ctx) : Option Nat :=
    let ctx := foo ctx (by apply h) -- This `(by apply h)`
    match _ : option_foo ctx (by grind [pred_foo]) with -- is a metavariable here, making grind fails
    | none => none
    | some ctx =>
      match _ : a with -- Without this seemingly unrelated match, there is no issue
      | some a => none
      | none => none

Steps to Reproduce

Here is a self-contained reproducer, with 2 workarounds:
https://live.lean-lang.org/#project=lean-nightly&codez=CYUwZgBADgTiwQBQEMIC4IDlkBcCU6EACjAPZToC8EAzqTDAJ4BQokYppSqG2+SAC0Kx4EZAV64qEAEaNa9Jq3ARyOAJakAdgH0OXFIT4FEQjCITjCAeSgbtWKWmpyFDFjgEh6IALbQ4YD1OYUCkfQgAYxwADwgBcgJAFMIA0Wi451l5OndmZUgcEBocJHTJfhQMW3stRwqzVIR0iQhqzVq+KmYIHogAGxAS9OkI4cRXZCgoPvkBAgBaeYg4aeRI9S0AcyQJqZn4ggB3dU94iDB1GKKITxAIdRoaAFcQbt7fXEihHUI1duCuGNXJsYBsEABtCwAgC6RxOQkWEBBYPOyHUfRoshAkWQTxod1ucHumNQvkGyAAbshQcgZAMxCVbhAAAbjeSTaazPDM/qkHE1N49AA+EC02julAAfKLxYKICK6GSorEIFK5T1EQAlPykCkbbaeB4QD44L7LHUU65Mh7PV69d6fb6EVDHTzq+UKJWoKUyrR2+0esV+1XSoOvfI3Io4ADq9AA1tTSE8tAhEGU6iZkFU7O0M4JQmlYi02g5Os45QMhirMqMVWyxHsuRBESs+mt9Tt2Y2DhBXUIhBcrpjrY8XnKTWafhg/toAcq4vXkSmIJDAjC4adEUuEGA0RisTi8QSvESjaTyVSaXS7lImazdpyDjy+nzcO05SKwyHff7hZ67sMPpfoimCkCUE4CB2DjMsgPJwL4upWl4xK2nkbCRsUsYwAmZDJsAgBBBKUsTlJm2Y1HmpgFk0RY2DmpZOJQFaDPOIwhECXaPnMzZLK27ZbJ2DacRu/bnJcSF3DaY72pWsjSDOui1guwKgsuq7wOu3EQAAsrqHZMhBoiFDA/gbGIECXuotL0hcMDFKJQ43Mhkm/sajoQFOsl9h+P7fmG3mKgBKpqgGmnagher8YamIQea4XiShUkBjFHkuvC7oKqQXq+bKIWfuK2V+kAA

def pred (a : Nat) : Prop := sorry
def foo (a : Nat) (h : pred a) : Nat := by sorry
def option_foo (a : Nat) (h : pred a) : Option Nat := by sorry
theorem pred_foo : pred (foo ctx hop) ↔ pred ctx := by sorry

def test (ctx: Nat) (a: Option Nat) (h : pred ctx) : Option Nat :=
    let ctx := foo ctx (by apply h) -- replacing (by apply h) with h fixes the issue
    match _ : option_foo ctx (by grind [pred_foo]) with -- grind fails because there is a metavariable at the `(by apply h)` location
    | none => none
    | some ctx =>
      -- Removing this match removes the issue
      match _ : a with
      | some a => none
      | none => none

-- First workaround
def testWorkaround (ctx: Nat) (a: Option Nat) (h : pred ctx) : Option Nat :=
    let ctx := foo ctx (by apply h) -- replacing (by apply h) with h fixes the issue
    match _ : option_foo ctx (by grind [pred_foo]) with -- grind fails because there is a metavariable at the `(by apply h)` location
    | none => none
    | some ctx => none -- Not matching on `a` removes the issue

-- Second workaround
def testWorkaround₂ (ctx: Nat) (a: Option Nat) (h : pred ctx) : Option Nat :=
    let ctx := foo ctx (by apply h) -- replacing (by apply h) with h fixes the issue
    let b := option_foo ctx (by grind [pred_foo]) -- Moving the matched term in a variable first fixes the issue
    match _ : b with
    | none => none
    | some ctx =>
      -- Removing this match removes the issue
      match _ : a with
      | some a => none
      | none => none`

Expected behavior: [Clear and concise description of what you expect to happen]

The (by grind [pred_foo]) line 8 should succeed, and no metavariable should be in the hypotheses when building this term.

Actual behavior: [Clear and concise description of what actually happens]

(by grind [pred_foo]) fails as there is a metavariable, with the error unknown metavariable ?_uniq.587`
Note that the bug is not due to grind, but rather to the metavariable being present.

Versions

4.28.0-nightly-2025-12-28
This was working before in 4.28.0-nightly-2025-12-09

Impact

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

[tobiasgrosser]

Thank you, @math-fehr.