Better warnings for duplicate instances

Stream: general

[David Loeffler]

Here's a thought that came to mind, when I was preparing a talk for my students.

A significant footgun for Lean coders (both novices & more experienced) is that when declaring typeclass arguments, you can easily end up with multiple competing copies of the same structures – e.g. two unrelated "add" operations on the same type – and the error messages when this happens are quite inscrutable: it will print a type mismatch error in which the expected type and the actual type have exactly the same string representation, which is baffling for the uninitiated.

This is a particular problem when working with Mathlib's typeclass hierarchy given that it currently has a slightly unpredictable mixture of "mix-in" classes (whose prereqs need to be explicitly declared) and classes implemented with extends, so this mistake is very easy to make.

Is there a way to make Lean specifically flag up whenever it finds itself trying to solve a unification problem involving two non-defeq instances of the same typeclass, and return a more comprehensible error message? Something like "warning: multiple non-defeq instances of [Add R] detected, check typeclass arguments"? (It would be even better if the message could summarize the synthesis paths leading to the conflicting instances.)

[David Loeffler]

(This is, of course, the same issue I raised earlier in #general > Multiple overlapping typeclasses. There I was asking if Lean could somehow automatically unify the duplicated type class assumptions. Here I’m asking for rather less: just that it should give more intelligible feedback to users to help fix the problem manually.)