Parameter implicitness in `derive` handlers

Stream: general

[Eric Wieser]

When I do

variables (G : Type*) (k : Type*) [semiring k]

@[derive [inhabited, add_comm_monoid]]
def add_monoid_algebra := G →₀ k

this results in a definition add_monoid_algebra.inhabited : Π (k : Type ?) (G : Type ?) [_inst_1 : semiring k], inhabited (add_monoid_algebra k G). Can derive be told to put k and G in {}?

[Floris van Doorn]

It probably could. Is that desirable? Since it's an instance, it won't be called to often manually, and I'm not sure if the heuristic "make all arguments implicit" is better than "use the same explicitness as in the main declaration".

[Eric Wieser]

In this case, it's because all the manual instances in the file use implicit parameters, so it feels inconsistent to switch them to derived instances

[Eric Wieser]

Frankly it feels like mathlib should have a convention for arguments to instances, and derive should match whatever that conclusion is

[Floris van Doorn]

Instances are almost never be written explicitly, so it tends to not matter whether the arguments are explicit. I have no good intuition whether I would want arguments explicit or implicit. My guess would be "explicit, unless a later argument depends on it."

[Mario Carneiro]

I generally try to use explicit arguments for instances, although they often inherit implicit from the variables declaration and it's not a big deal like Floris said. The primary advantage of being explicit is that it's easier to see what's going on when you print them out

[Mario Carneiro]

also it's generally less typing if for whatever reason you need to specify a typeclass instance