RFC: Make "synthesized TC instance not defeq to expression inferred by typing" error easier to debug

Proposal

Consider the following MWE:

class MeasurableSpace (α : Type) where
  foo : Nat

structure Kernel (α β : Type) [MeasurableSpace α] [MeasurableSpace β] where

def myKernel (α : Type) {noncanonical : MeasurableSpace α} [canonical : MeasurableSpace α] :
    @Kernel α α noncanonical canonical where

/-
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  canonical
inferred
  noncanonical
-/

Where the error is coming from is quite subtle for the untrained eye: One could think that nothing was written in the body of the definition yet! And the error message doesn't help as it doesn't say which argument to which function it happened in.

Here for context, the error comes from Kernel.mk having type ∀ {α β} [MeasurableSpace α] [MeasurableSpace β], ... and me trying to feed in the [MeasurableSpace α] argument while there are two such hypotheses in context.

Could the error message be similar to the "application type mismatch" error, which would give something like

type class synthesization mismatch
  @Kernel.mk α α canonical
argument
  canonical
but by typing rules it was inferred to be
  noncanonical

with possibly "typing rules" replaced by "unification".

Community Feedback

Zulip. In short: Eric suggested #5085, I suggested the above.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with the minimal working example in the issue and reproduce the synthesized type class instance error involving Kernel.mk, canonical, and noncanonical. Trace the diagnostic path that emits this message; done means the error identifies the application and argument mismatch in a form comparable to the proposed example.