Style: shadowing instance variables in instance declarations

Stream: mathlib4

[Thomas Murrills]

In experimenting with the upcoming overlapping variables linter in #34955, it became apparent that it's (reasonably) common style to shadow instance variables when declaring an instance, e.g.:

variable {A} [Foo A] [Bar A]

instance [Foo A] [Bar A] : Baz A where ...

This means that in the local context in the fields of Baz, the instances are duplicated. The actual resulting declaration is (I believe) fine, though. (I.e. it does not wind up with duplicate instances, since lean only takes the ones that are used).

How do we feel about this? On the one hand, I feel like duplicating instances in a local context is not great. Specifically, I'd weakly prefer not using variable before instance, so you can still always see the instances required explicitly for an instance, but do not duplicate them in the local context. But...I would also love to not have to restructure this linter. :) So I worry that that makes me biased, and that my sense that not shadowing variables is actually nicer is merely an artifact of its benefit to me.

So, what do you think? Is it reasonable for this linter to discourage this sort of instance hypothesis shadowing, or should it stay silent in cases like this?

[Aaron Liu]

What's the reason for duplicating the instance assumptions at the instance declaration?

[Thomas Murrills]

I'm assuming the goal is showing in source more clearly which instances let you synthesize this instance, but I'm just inferring this based on the fact that it turns out to be common enough to produce a ton of linter violations. (Sometimes the variable is further up, with some commands in between.)

But it is possible it's just a bunch of oversights! :)

[Yury G. Kudryashov]

My guess is that it should be an oversight in most cases.

[Edward van de Meent]

Could it be the case that sometimes it is caused by weakening or strengthening assumptions? e.g. assuming CommRing when in the context we have Ring or vice versa?

[Ruben Van de Velde]

That sounds like it would go wrong unless you also redeclare the A, right?

[Ruben Van de Velde]

Sometimes for defs I think it happens to make the type argument explicit

[Edward van de Meent]

Ruben Van de Velde said:

That sounds like it would go wrong unless you also redeclare the A, right?

I think it merely could go wrong, it doesn't guarantee issues.

[Thomas Murrills]

Ok, great. :) Based on sampling a handful of errors, it seems that they are by and large merely duplicated, not weakened.

Do we feel strongly about whether the hypotheses should be in variable or instance? If not, my general rule in fixing these will be:

If there aren't very many instance hypotheses and the offending instance declaration is at the beginning/end of a section, keep inlined hypotheses and remove variable. Otherwise, keep the variable hypotheses and remove them from instance.

[Thomas Murrills]

Linter-independent fixes in this direction are now in #35002, #35003, #35006, and #35007. After these, Mathlib should be ready for the overlapping instances linter, modulo a small handful of declarations.