diamond linter

Stream: mathlib4

[Johan Commelin]

But maybe that should be generalized to a much larger class of instances...

We see questions regularly where someone has [AddGroup R] [Ring R]. And a syntax linter could flag: hey, you now have two different ways to synth Add R, namely these two paths: ..., ...

[Thomas Murrills]

Ah, I see...that sounds quite costly :grinning_face_with_smiling_eyes: I'm guessing it's not specific to DecidableEq either, right?

[Thomas Murrills]

Maybe we could curate (or better, automatically construct) a collection of common diamonds, so that we get some benefit but are still performant? :thinking:

[Thomas Murrills]

(My thinking is that a fully general diamond detector would need to simply try to re-synthesize various instances after turning some others off one by one, and that this would be too costly.)

[Matthew Ballard]

What does variable? do?

[Kenny Lau]

@Thomas Murrills should we move this to another thread? (in new thread: I'm not sure if this is a good idea, but we could have some "forward instance" machinery infrastructure so that given Ring A then the machine generates AddCommMonoid A etc, and then we compare those instances, but then this also sounds very expensive...; alternatively, we store by hand the various "extends" relation for this forward instance implementation, because sometimes we might want more than "extends"; or maybe "extends" is enough and we can try to see where that leads us first?)

[Thomas Murrills]

(I don't think I have Zulip permissions to do so, but I encourage someone who does to move the messages! :grinning_face_with_smiling_eyes:)

[Jireh Loreaux]

I think what we could have that isn't too expensive, and that would catch the most common paper cuts, including the two mentioned above, is this: For each explicit [Foo] in context, consider only data-carrying structure projections (transitive closure included) of Foo. If two instances in context, say Foo and Bar, have a data-carrying class Baz in common, then the linter complains. Given that we use forgetful inheritance, I think this should catch mistakes. It obviously won't be able to detect "true diamonds", but I think we don't actually care.

It would be nice to have this linter on, at least in CI, hat would process each declaration, but it would also be nice to have a command / tactic to call it independently as a sanity check for yourself. I think this would be a huge benefit to new users especially.

[Notification Bot]

8 messages were moved here from #PR reviews > #29422 [LinearOrder α] [DecidableEq α] by Johan Commelin.

[Damiano Testa]

I wrote a linter that did that, started fixing the exceptions, but I remember that there were many exceptions.

[Damiano Testa]

#14731, I think.

[Jireh Loreaux]

If seems like Matthew had the same idea there as mine above. Your linter seems to be doing much more work than I'm going for.