unknown free variable in unreachable pattern

[eric-wieser]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] 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

The following:

def ohno (x : List (Fin 2)) : Nat :=
  match x with
  | [⟨0, _⟩] => sorry
  | [1] => sorry
  | [x] => sorry
  | _ => sorry

fails with unknown free variable '_fvar.113'.

Context

Discovered while helping with #new members > ✔ pattern matching on `Finset (Fin _)` @ 💬

Steps to Reproduce

1. Run the above code

Expected behavior: No error, or perhaps a warning that [x] is unreachable.

Actual behavior: The error reported above.

Versions

Lean 4.21.0-nightly-2025-06-02 Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

[adomani]

You don't even need the list:

def ohno (x : Fin 2) : Nat :=
  match x with
  | ⟨0, _⟩ => sorry
  | 1 => sorry
  | x => sorry
  | _ => sorry

gives also an unknown free variable error.

[SnirBroshi]

The error is no longer "unknown free variable", now it's:

Failed to compile pattern matching: Stuck at
  remaining variables: [x✝:(Fin 2)]
  alternatives:
    [isLt✝:(0 < 2)] |- [(Fin.mk 0 isLt✝)] => h_1 isLt✝
    [] |- [1] => h_2 ()
    [x:(Fin 2)] |- [x] => h_3 x
    [x✝:(Fin 2)] |- [x✝] => h_4 x✝
  examples:_

[nomeata]

So this seems to be due to mixing Fin constructors and Fin literals maybe. Is this blocking anyone?