Linter rejects automatic instance

Stream: general

[Bhavik Mehta]

In the following file, the unused arguments linter complains about #print f.decidable_eq /- argument 2: [a : decidable_eq J] -/ having an unused argument - is it possible to change how the derive works to avoid this?

import tactic

variable (J : Type)

def mytype (J : Type) : Type := option J

@[derive decidable_eq]
inductive f : mytype J → Type
| a : f none

#lint

[Bhavik Mehta]

Cf my PR https://github.com/leanprover-community/mathlib/pull/2461

[Kevin Buzzard]

hmm I think this might be a known issue

[Scott Morrison]

@Bhavik Mehta, could you create an issue for this? We should track it.

[Bhavik Mehta]

Looking at https://github.com/leanprover-community/mathlib/issues/1077, it seems to be a lean issue rather than a mathlib issue...

[Bryan Gin-ge Chen]

Is there a related open issue on the community Lean repository?

[Bhavik Mehta]

Doesn't seem like it

[Kevin Buzzard]

Sorry, when I said known issue I literally just meant "I think someone mentioned it on the chat once". I forgot that an issue was a real thing

[Rob Lewis]

This is unrelated to #1077. For now you can do attribute [nolint unused_arguments] f.decidable_eq. This is probably fixable, probably not trivial. The decidable_eq derive handler is in core so it's an issue there.