Field notation for abbreviations fails if the argument is an optParam

[kmill]

Description

If the receiver of generalized field notation is an optional parameter then it fails to resolve the field notation for type abbreviations.

This is because it's using consumeMData rather than cleanupAnnotations in Lean.Elab.Term.typeMatchesBaseName.

Context

This is not an important bug, and I doubt it is affecting anyone, but it's easy to fix. Type abbreviations are used for overriding methods for field notation in mathlib, but not while using optional parameters.

Steps to Reproduce

structure A

abbrev B := A

def A.x (_ : A) := 1
def B.x (_ : B) := 2

def A.y (_ : A) := 1
def B.y (_ : B := {}) := 2

#eval (show A from {}).x -- 1
#eval (show B from {}).x -- 2
#eval (show A from {}).y -- 1
#eval (show B from {}).y -- fails, should be 2
/-
invalid field notation, function 'B.y' does not have argument
with type (B ...) that can be used, it must be explicit
or implicit with a unique name
-/

Versions

4.7.0-rc2
macOS 14.4

Impact

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