Higher order constructor field needs to be given explicitly in match patterns

Description

If a pattern in a match involves an implicit higher-order field that appears in an index, then an "invalid pattern" error is reported. It needs to be provided explicitly.

Context

Reported on Zulip: #new members > Possible pattern matching bug? @ 💬

Steps to Reproduce

In the following, test' works and has f provided explicitly, but when it is implicit in test there is an "invalid pattern" error.

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

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

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

Note that this gives the same invalid pattern error, so it's not a property of dot ident notation:

def test {n : Nat} : Foo n → Foo n := fun
  | Foo.proj i => sorry

Versions

Lean 4.22.0-rc4
Target: x86_64-unknown-linux-gnu

Impact

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

Reproduce the issue with Lean 4.22.0-rc4 using the Foo inductive type and the test/test' definitions in the report. Compare the explicit (f := f) pattern with the implicit .proj i and Foo.proj i forms. Done means the implicit higher-order field is handled without an "invalid pattern" error.