Structure update notation falls over optional parameters

[nomeata]

Description

In the following code, I’d expect { m with a := id } to work, but the elaboration falls over copying the other field over.

structure Methods where
  a : Int → Int
  b : Nat → (opt : Nat := 42) → Nat


/--
error: type mismatch
  fun a => m.b a
has type
  Nat → Nat : Type
but is expected to have type
  Nat → optParam Nat 42 → Nat : Type
-/
#guard_msgs in
def f (m : Methods) : Methods := { m with a := id }

/--
error: type mismatch
  fun a => m.b a
has type
  Nat → Nat : Type
but is expected to have type
  Nat → optParam Nat 42 → Nat : Type
-/
#guard_msgs in
def g (m : Methods) : Methods := { m with a := id, b := m.b }

def h (m : Methods) : Methods := { m with a := id, b := @Methods.b m }

Maybe related to #5397?

Versions

4.12.0-nightly-2024-09-19

Impact

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

[Kha]

(the simplest fix may be to support @m.b if that is generally desirable)