Typeclass inference fails if argument is a `match`

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

Typeclass inference fails unexpectedly if an argument is a match.

Context

No relevant context.

Steps to Reproduce

Consider the following input:

class Test (n : Nat)

instance {n} : Test n := ⟨⟩

-- works
#synth Test 1
-- fails
#synth Test (match ?_ with | 0 => 1 | _ => 1)
-- works
#synth Test (if ?_ == 0 then 1 else 1)

(This repro was originally posted by lzy0505 here.)

Expected behavior: Inference succeeds.

Actual behavior: Inference fails.

Versions

Lean 4.29.0-nightly-2026-02-08
Target: x86_64-unknown-linux-gnu

Additional Information

None.

Impact

Both lzy0505 and myself bumped into this while using iris-lean. The bug means that Iris theorems of the form P \vdash Q where P is a match are not easy to use in iris-lean.

Start with the minimal #synth reproduction in the issue and trace how typeclass inference handles the match expression, comparing it with the working if expression. Confirm the change against the shown Test instance and verify that inference succeeds for Test (match ?_ with | 0 => 1 | _ => 1) without Mathlib or Batteries.