RFC: Turn "synthesized TC instance not defeq to expression inferred by typing" error into a disableable warning

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
-/

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.

This is a very common setup in probability theory, where one sigma-algebra (aka MeasurableSpace instance) is canonical and we use one or several sigma-subalgebras of that canonical one to represent information evolving over time/space. Probability theory in Mathlib so far has mostly avoided those situations, but things are starting to change:

• People like Jason Kexing Ying are pushing for martingales (information evolving over time)
• I am involved in the project of setting up Gibbs measures (information evolving in space)

On the basis that Lean could do what I meant above, but decided to error anyway, it would be great if

1. The error above were merely a warning
2. That warning were disableable, so that people like me can say "I know what I'm doing" and ignore it

Community Feedback

Zulip. In short: Eric suggested the above, I suggested to make the error easier to debug (#5086).

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 MWE and the type of Kernel.mk, focusing on the synthesized and inferred MeasurableSpace instances described in the issue. Trace where this mismatch becomes an error and determine the warning configuration mechanism. Done means the diagnostic is a disableable warning rather than an unconditional error.