Detecting typeclass clashes

Stream: new members

[Stuart Presnell]

Is there any way to automatically detect and warn about typeclass errors where, for example, you've accidentally introduced two zeroes for a type? This sort of error leads to failures that are pretty cryptic for a beginner, and I'm wondering if there's any way to make it more obvious what's going wrong.

[Anne Baanen]

This would indeed be very helpful, but I don't think we have anything in that direction.

[Yaël Dillies]

There has been discussion about this, but nobody spent time on it yet.

[Alex J. Best]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Stupid.20assumptions.20tactic/near/264155485, its certainly related to a lot of things I've been trying recently, and it sounds nice, its just not clear how it would be used. Like if its a tactic people have to call I'm not sure it will help beginners (who will teach them the tactic!)

[Alex J. Best]

Maybe a more useful thing to do is to add nice doc pages with common debugging tips for specific errors, and then link to them from the lean error messages themselves

[Stuart Presnell]

I was thinking of it as a command like #lint that you could invoke to check for typeclass conflicts. Absolute beginners might not know about it at first (because they don’t know anything at first!) but once you know it’s there it would be a useful tool for resolving mysterious proof failures.

[Stuart Presnell]

But yes, good debugging documentation would also be very helpful.