Failure to create instance in presence of multiple default fields

[oskgo]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Some type classes with multiple default fields cannot be instanced without providing any of the default fields.

Steps to Reproduce

class Cls (T : Type) where
  ITy: Type := Unit
  cst: ITy
  map (_: ITy) : ITy := cst

def Ty: Type := Unit

instance : Cls Ty where
  cst := ()

Actual behavior:

The code fails with the error fields missing: 'map'. Adding either map or ITy definitions to the instance works.

Expected behavior:

The code should generate an instance of Cls Ty. There's a workaround (other than repeating the defaults) using functions with default arguments that demonstrates that this should be reasonable to expect;

def makeintance {T: Type} (ITy: Type := Unit) (cst: ITy) 
    (map: ITy -> ITy := λ _ => cst) := @Cls.mk T ITy cst map

instance : Cls Ty := makeintance (cst:=())

This works as you would expect.

Versions

Lean (version 4.0.0-nightly-2023-04-20, commit f9da1d8, Release)
Windows 11

[Kha]

Works on master!