It's difficult to design a language that has implicit arguments *and* allows you to explicitly instantiate them. Agda has done very admirably.
But I do not like bound names, which are often single letters, getting undeservedly elevated to names that play a descriptive role.
My maxim is:
If you see {A = A} in an argument list, they blew it.
There is something very honest about the way this is dealt with in Rocq, oversimplified below:
1. Implicitness of arguments is a "calling convention" that is configured for each defined function.
2. If you want to deviate from the implicit calling convention of a named function, you use an `@` sigil before the function, and then all arguments become explicit.
I like this a bit more because it discourages you from making things implicit that you frequently have to supply explicitly. Very quickly you learn whether your API is realistic in light of the unifier.
Jon Sterling
David Berry