local instances in #lint

Stream: std4

[Matthew Ballard]

The defLemma linter is giving false positives on local instances for Prop-valued classes, like Fact. An example pops up in #6149.

How does one read the local instances in general?

[Alex J. Best]

I don't think this is a false positive per se, really the problem is the fact that instance is always a def even when it is prop valued, and this should at some point change (but its probably a core change). We _could_ make the linter check if the type of a declaration is a class, rather than checking if the declaration itselft is tagged as an instance to avoid them being reported for now. But imo these defs that should be lemmas really are defs that should be lemmas, not false positives.
Until then using @[local instance] theorem isScalarTower_S_right := sorry seems fine to me

[Matthew Ballard]

I agree that is a worse problem. But apparently defLemma is already working around the problem with a regular instance.

[Alex J. Best]

Right its manually working around this by skipping global instances, but as far as I know Std.Tactic.Lint doesn't have access to the information of which local instances were set in some section somewhere in the library, so my suggestion of skipping all class valued defs would be the only way to make this happen. But why work around the issue if we can use @[local instance] theorem in place of local instance and get library that doesnt have this isuee.

[Matthew Ballard]

Can we get the local context from declaration and find the local instances that way? (This is more about curiosity than anything. I am fine with any solution.)

[Mario Carneiro]

notice the comment in docBlame:

    if (← isAutoDecl declName) || isGlobalInstance (← getEnv) declName then
      return none -- FIXME: scoped/local instances should also not be linted

The information that something is defined as a scoped/local something or other is not stored in a sufficiently permanent way for #lint to tell. In theory you could work it out for scoped instances but you would have to check every namespace, it's not suitably indexed at all. For local instances the info is gone, I'm pretty sure it is impossible

[Eric Wieser]

Is the core change to make instance use theorem controversial, or just low priority?

[Eric Wieser]

And is switching mathlib to use @[instance] theorem instead of instance more or less controversial?

[Matthew Ballard]

How would the core change be done in theory? Can you figure out whether you have a Prop or not in CommandElab?

For the latter, I think you want to switch to @[instance] def for uniformity also.

[Mario Carneiro]

Eric Wieser said:

Is the core change to make instance use theorem controversial, or just low priority?

it's fine by me. IIRC core accepted a patch to make nested recursive functions (let rec & where) handle def/theorem correctly not too long ago, so I think this wouldn't be too different