incorrect_type_class_argument linter

Stream: general

[Sebastien Gouezel]

I would like to define something which is not a class, but use it as a class in a part of a development. Typically something like

import data.nat.basic

/-- Something which is not a class, but that I will use locally as a class -/
def not_class (n : ℕ) : Prop := (n = n)

section

local attribute [class] not_class

/-- I want to use `not_class` as a class here. -/
@[nolint incorrect_type_class_argument unused_arguments]
def use_class (n : ℕ) [not_class n] : ℕ := n

end

This works well, except that the linter complains:

/- INCORRECT TYPE-CLASS ARGUMENTS.
Some declarations have non-classes between [square brackets]: -/
#print use_class.equations._eqn_1 /- These are not classes. argument 2: [_inst_1 : not_class n] -/

What is the right way to tell the linter that, really, I know what I am doing here?

[Rob Lewis]

I guess use_class will be useless outside of this section, right? Can you make it private?

[Rob Lewis]

Hmm, private declarations seem to be included in that lint, that doesn't seem right.

[Reid Barton]

Maybe it would make more sense to just implement this test in Lean itself?

[Reid Barton]

Why is it linting the autogenerated equational lemma?

[Rob Lewis]

Some linters apply to all declarations including the autogenerated ones. This one probably shouldn't.

[Sebastien Gouezel]

Ideally, if I disable a linter for a def, then it should be disabled also for its equational lemmas.

[Sebastien Gouezel]

Thanks @Rob Lewis for #3006. Shortest (and most efficient) PR ever?