request: document behavior of implicit arguments in generalizing binders

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4041
From: @mikeshulman
Reported version: trunk
CC: coq-bugs-redist@lists.gforge.inria.fr

[coqbot]

Comment author: @mikeshulman

It seems that when using implicitly generalizing binders, the arguments of the type of the variable being bound have their implicit status frobbed in some way that I do not understand. For instance, we have to write `{IsEquiv _ _ f} when it appears inside a generalizing binder, whereas normally the first two arguments are implicit and we can simply write IsEquiv f. On the other hand, it seems that sometimes an argument that is normally explicit gets made implicit inside the generalizing binders (maybe when it's a typeclass?). Also, while we have to write `{IsEquiv _ _ f}, if f is a family of morphisms we can write `{forall a, IsEquiv (f a)}. It would be nice to have some documentation of what is going on here (and hopefully an explanation for the motivation).

[SkySkimmer]

https://coq.github.io/doc/master/refman/language/extensions/implicit-arguments.html#implicit-generalization

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. Other arguments are also generalized unless provided. This produces a fully general statement. this behavior may be disabled by prefixing the type with a ! or by forcing the typeclass name to be an explicit application using @ (however the later ignores implicit argument information).

[mikeshulman]

I would not realize from reading that paragraph that non-typeclass originally-implicit arguments of the type are no longer implicit inside a generalizing binder, unless I already knew it.

[mikeshulman]

It seems that the point is that the declared implicitness or explicitness of arguments is essentially ignored inside a generalizing binder, being replaced by "all typeclass arguments are implicit while all others are explicit, but if it is only partially applied then the missing arguments are also implicitly added". Is that right?

I do think it would also be helpful to mention explicitly that this frobnification doesn't apply to universally quantified typeclasses, because in other contexts those are treated similarly to ordinary typeclasses.