definitions generated by `deriving DecideableEq` or `deriving Repr` trigger the Batteries unused arguments linter

[kim-em]

See for example Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

[nomeata]

This is since #10271

Not sure if that's a bug in the code: the class determines the signature of the methods, so I cannot drop the arguments here. Or is there an easy way to please the linter?

[nomeata]

Ah, now I see the discusion on zulip.

I see in this example we previously had

-- This is relying on an automatically generated instance name, generated in a `deriving` handler.
-- See https://github.com/leanprover/lean4/issues/2343
attribute [nolint unusedArguments] instDecidableEqHom

But do we want to fix this more fundamentally?

Given

attribute [nolint unusedArguments] instDecidableEqHom

the linter could apply this nolint to all definitions under instDecidableEqHom.

This seems generally a reasonable thing to do for a linter: If it should not look at foo, then maybe it shoudn’t look at auxillary definitions that belong to foo, e.g. those in where. (At least if foo is a definition and not a type.)

[nomeata]

Or is there a way to make the definition pass the linter? Use an underscore somewhere?

[nomeata]

Looking at the linter code, I don’t see a provision for this (e.g. not warning about function arguments with a user name _, indicating that the programmer intended to have an unused argument). Maybe this could be added, and the deriving code adjusted to set the user name to _ if it’s unused?

Alternatively batteries could try to treat these as isAutoDecl; not sure if that’s the right call though.

[urkud]

Why does this instance

def CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq.{u_1} : {J : Type u_1} →
  {a a_1 : WidePullbackShape J} → [DecidableEq J] → (x x_1 : a.Hom a_1) → Decidable (x = x_1) :=
fun {J} {a a_1} [DecidableEq J] x x_1 ↦
  match a, a_1, x, x_1 with
  | a, .(a), Hom.id .(a), Hom.id .(a) => isTrue ⋯
  | .(some a), .(none), Hom.term a, Hom.term .(a) => isTrue ⋯

requires [DecidableEq J]? BTW, it always returns isTrue, i.e., it's a Subsingleton. Does it make sense to autodetect this and return isTrue <| match ...?

[nomeata]

It's always been like that that derived instances have rather naive assumptions. But until recently the implementation function had an inaccessible name, so probably nobody noticed. Changing the implementation should be a separate discussion from this one about the linter, though, I think.

[urkud]

I think that as long as the autogenerated DecidableEq instances have unused arguments, the linter should complain about them. I wouldn't silence the linter just to avoid @[nolint] lines. @kim-em What were your intentions for this issue: silence the linter or fix the autogenerated def? It isn't clear from the description.

[hrmacbeth]

Just came across this again with https://github.com/leanprover-community/mathlib4/pull/29982.