"This pattern contains metavariables" when using structure constructor and omitting a proof parameter

Description

When using a match for a structure that has a proof parameter and a pattern that uses the constructor directly, there is an "Invalid match expression: This pattern contains metavariables" error.

This causes many deriving handlers to fail, such as DecidableEq (see Additional Information).

Context

This is triggered by the Mathlib derive Fintype handler, which elaborates a match using constructors directly. This was noticed in #mathlib4 > `deriving Fintype` with Prop @ 💬

Steps to Reproduce

structure MyStruct (p : Nat) (h : p < 10) : Type where
  P : Fin p

def MyStruct.P1 {p : Nat} {h : p < 10} : MyStruct p h → Fin p
  | MyStruct.mk P => P
/-  ~~~~~~~~~~~~~
Invalid match expression: This pattern contains metavariables:
  { P := P }
-/

def MyStruct.P2 {p : Nat} {h : p < 10} : MyStruct p h → Fin p
  | @MyStruct.mk _ _ P => P
/-  ~~~~~~~~~~~~~~~~~~
Invalid match expression: This pattern contains metavariables:
  { P := P }
-/

-- Succeeds:
def MyStruct.P3 {p : Nat} {h : p < 10} : MyStruct p h → Fin p
  | { P } => P

Expected behavior: All three definitions elaborate without errors.

Actual behavior: Only the third definition elaborates without errors.

Versions

Lean 4.27.0-rc1
Target: x86_64-unknown-linux-gnu

Additional Information

The structure instance notation elaborator appears to be propagating the proof parameter h into argument 2, but the application notation elaborator is not. It's not clear why this is happening (maybe it's due to structure instance notation elaboration postponing elaboration?). This isn't diagnosing the issue however — I think the match notation elaborator itself isn't propagating the expected type into the pattern here.

The issue affects many deriving handlers. For example, DecidableEq:

structure MyStruct (p : Nat) (h : p < 10) : Type where
  P : Fin p
  deriving DecidableEq
/-         ~~~~~~~~~~~
Invalid match expression: This pattern contains metavariables:
  { P := a✝ }
-/

Impact

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

Start with the MyStruct.P1, P2, and P3 reproductions and inspect the match notation elaborator, alongside the structure instance notation elaborator mentioned in the report. Done means all three definitions elaborate without metavariable errors and deriving DecidableEq succeeds for the structure with a proof parameter.