self and explicitVarsOfIff linter

Stream: general

[Chris Henson]

I find this lint for bundled structures counter-intuitive:

import Batteries

structure Foo where
  P : Prop
  iff : P ↔ P

/-- info: Foo.iff (self : Foo) : self.P ↔ self.P -/
#guard_msgs in #check Foo.iff

-- complains about `self` being explicit
#lint- only explicitVarsOfIff

Any Iff that references the structure on both sides will have this issue. Maybe a potential improvement to the linter?

[Eric Wieser]

This more looks like a feature request (for Lean itself) to allow overriding the argument explicitness of self in fields

[Chris Henson]

That makes sense, related to #lean4 > RFC: adjust argument explicitness on typeclass projections I guess?