Linter for overlapping instances

Stream: mathlib4

[Jovan Gerbscheid]

A common stumbling block when using type classes is that things go wrong when you have multiple data carrying local instances carrying different copies of the same data. This came up again today:

Kim Morrison said:

We really really need a linter for this.

So, I took a stab at writing such a linter. The code is in #33677.

And here's the list of the 84 current offenders: https://gist.github.com/JovanGerb/f104519064aa2d902dde64693e8341a3

[Johan Commelin]

This is an environment linter, right? Could it be made a syntax linter, so that it gives feedback when writing the code, instead of when submitting a PR?

[Damiano Testa]

There was also #14731, although that is really outdated now.

[Thomas Murrills]

Hi Jovan! This looks great! Would you like to collaborate on making it a syntax linter? I think I can reuse some components used in the unusedInstancesInType linters to turn it into one without too much trouble.

[Jovan Gerbscheid]

@Thomas Murrills yes, I would be happy to! I haven't made a syntax linter before. How hard is it for it to get access to the type of the declaration? In a perfect world, the linter would be able to run as soon as the type of a theorem has been written, without a proof, or with a partial proof.

[Thomas Murrills]

This particular task feels like a bit of a hack, but is ultimately sort of doable! :)

What we (can) do is look through the infotrees for a Lean.Elab.BodyInfo representing the body. I believe this should be present even in the case of partial proofs, but haven't checked. Its child is a TermInfo, PartialTermInfo, or TacticInfo, which has a local context and expected type we can use (one way or another)!

[Jovan Gerbscheid]

Nice! A local context is all that we need for this linter.

[Thomas Murrills]

Alternatively, we can simply get the name of the declaration from the parentDecl at this point, and look for that in the environment. docs#Lean.Elab.InfoTree.getDeclsByBody However, I'm not sure if that works with partial proofs. This was the strategy I took in the unused instances in type linters, because (1) it was the simplest to implement and review (2) it was actually better performance-wise to use the type directly.

[Thomas Murrills]

Shall I make a PR to your branch? Or, do you want to try writing your first syntax linter? :) Or! I could review your environment linter PR, and then you could review my syntax linter PR (which would be based on your environment linter infrastructure). I'm happy with any one of these! :)

[Jovan Gerbscheid]

Feel free to make a PR to my PR :)

[Alex Meiburg]

the biggest crime in that list is having a declaration simply known as docs#impl

[Kim Morrison]

My fault! :-) At least it is already deprecated.

Can I say again: please, please, can we namespace Mathlib? :-)

[Notification Bot]

4 messages were moved from this topic to #mathlib4 > Namespacing Mathlib by Thomas Murrills.