request : intelligent implicit generalization

[jonleivent]

The documetation of backquote implicit generalization states:

When generalizing a binder whose type is a typeclass, its own class arguments are omitted from the syntax and are generalized using automatic names, without instance search.

It would be nice to have a similar mechanism that does instance search first, deciding to generalize only those typeclass binder requirements that cannot be fulfilled in the current context, such as by preceding arguments.

Suppose we have 3 standalone typeclasses, 2 dependent typeclasses and a function definition that uses those 2:

Class C1 ... := ...
Class C2 ... := ...
Class C3 ... := ...
Class C4`{C1,C2} := ...
Class C5`{C1,C3} := ....
Definition f <arglist with C4 and C5> := ...

The problem is with conveniently specifying the arglist of f. Saying:

Definition f `{C4,C5} := ...

means that the instances for C4 and C5 do not share the instance of C1, which may cause issues within the definition of f. Saying instead:

Definition f `{C4,!C5} := ...

does not work because C3 is missing, as C5 is not generalized over at all. Reversing the order of C4 and C5 does not help because it produces a symmetric problem involving C2 instead of C3.

Currently, there is no way to accomplish this without explicitly naming C3 (or C2 if the order is reversed).

This request is for some convenient mechanism to implicitly generalize C5 over what can't be found by typeclass search at the point where the C5 argument appears, in this case only C3 because C1 is already provided by the generalization of C4.

[Alizter]

Yes, I've wanted something like this for a while. It can be very annoying to have to list a whole hierarchy explicitly because two classes use the same instance.