Isn’t it already what’s meant by this paragraph?
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.
and reinforced by:
this behaviour 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).
Where does that say that this ignores the implicit status of arguments? See for example
Class tc_def2 {H:False} := mkDef2 : Type.
Generalizable All Variables.
Section test.
Context `{tc_def2 X}. (* implicit argument became explicit?? *)
I would expect this to error because tc_def2's only argument is implicit. But this gets accepted.
Alright, I had misunderstood what you meant. This is weird indeed, and looks like a bug.
Maybe a documentation bug, I don’t know if there’s a sensible way to handle implicits together with the rest of the feature.