simp linter and structure fields

Stream: general

[Sebastien Gouezel]

@Gabriel Ebner , I am surprised by the simp lint behavior in the following example:

import data.equiv.basic

variables {α β : Type}

structure my_equiv (α : Type*) (β : Type*) :=
(to_fun     : α → β)
(inv_fun    : β → α)
(left_inv   : ∀x, inv_fun (to_fun x) = x)
(right_inv  : ∀x, to_fun (inv_fun x) = x)

attribute [simp] my_equiv.left_inv

instance : has_coe_to_fun (my_equiv α β) := ⟨_, my_equiv.to_fun⟩

@[simp] lemma my_equiv_apply (e : my_equiv α β) : e.to_fun = e := rfl

#lint -- does not complain that my_equiv.left_inv should not be a simp lemma

@[simp] lemma should_not_work (e : my_equiv α β) (x : α) : e.inv_fun (e.to_fun x) = x :=
e.left_inv x

#lint -- does rightly complain that should_not_work should not be a simp lemma

I put an attribute simp on a field of a structure, here my_equiv.left_inv. But then I declare a simp normal form using a coercion, which means that my_equiv.left_inv will never fire. The linter doesn't complain about this, while it does if I the simp attribute is on a lemma saying exactly the same thing.

[Gabriel Ebner]

Mmh, the linting error would be on my_equiv.left_inv but I guess we don't lint that declaration because it is automatically generated. @Rob Lewis @Floris van Doorn Should we lint constructors and projections as well?

[Sebastien Gouezel]

In the case of simp attributes, it is a conscious decision to put it on the field, not something done under the hood, so I think it would deserve being reported by the linter.

[Rob Lewis]

Maybe it should be a choice made for each linter, like we do for auto decls?

[Rob Lewis]

It doesn't make sense to check constructions for doc strings.

[Gabriel Ebner]

I think that's the only one, I'll just add the check there. There are some declarations that we never want to look at like sizeof or the general inductive encoding. Should we lint brec_on and company?

[Rob Lewis]

Is there really that much to gain though? Besides the simp linters, what do we expect to catch by linting these things? You can only fix them by changing a different declaration, and usually the error would show up there already, no?

[Gabriel Ebner]

I completely forgot that we already have an auto_decls flag in the linters to opt-in to auto decls. I'll try to enable it for all linters where it seems reasonable.

[Gabriel Ebner]

Some (but not all) of the type class linters already had this flag set.

[Gabriel Ebner]

I forgot to mention this, but my_equiv_apply actually does not make my_equiv.left_inv redundant! This is because my_equiv_apply is only defined for Type 0, while my_equiv.left_inv works in all universes.

[Sebastien Gouezel]

My mistake, I should have put Type* everywhere. It doesn't change the output of the linter, though.

[Gabriel Ebner]

That's what #2580 is for. :smile:

[Sebastien Gouezel]

Thanks!