simp lemma with variable head

Stream: lean4

[David Wärn]

Because of changes in simp's indexing (if I understand correctly), in Lean 4 we can now write code like

class HasInv (f : α → β) where
  (inv : β → α)
  (self_inv : ∀ b, f (inv b) = b)
open HasInv
attribute [simp] self_inv
example (f : α → β) [HasInv f] (b : β) : f (inv f b) = b := by simp

In Lean 3, simp would never use self_inv since the head f of the lhs is a variable.

But when I lint the example above in std4, both the simpNF linter and the simpVarHead linter throw errors. Is this as it should be? I thought the new simp was smart enough to only try to apply self_inv when IsEquiv.inv appears somewhere?

[Sina]

just a naive question, what is std4?

[Alex J. Best]

Its the project https://github.com/leanprover/std4#std4, a standard library for lean 4, containing generally useful material for lean 4 projects that isn't central enough to make it into the core lean itself

[Gabriel Ebner]

The new simp hasn't changed in that regard. The lhs of self_inv is still a badly conditioned HO pattern, ?f (inv ?f ?b) ?b. The unifier will choke on it, and we can't index it either.