Possible pattern matching bug?

Stream: new members

[Fernando Chu]

Is this behavior expected?

import Mathlib

inductive Foo : ℕ → Type where
  | proj {n} {f : Fin n → ℕ} (i : Fin n) : Foo (f i)

-- Works
def test' {n : ℕ} : Foo n → Foo n := fun
  | .proj (f := f) i => sorry

-- Invalid pattern ?m.2299 i
def test {n : ℕ} : Foo n → Foo n := fun
  | .proj i => sorry

Why do I have to specify f above?

[Kyle Miller]

Not sure, and it seems like it's potentially a bug. Reported it: lean#9617