::> only declares an instance without a coercion when it should do both

[Alizter]

Description of the problem

There is a difference in behaviour of ::> when in a record or in an class. In both cases ::> is expected to register an instance and a coercion.

When ::> is given in a record, it works as expected. However when ::> is given in a class, only the instance is declared and the coercion is ignored.

cc @proux01

Small Coq file to reproduce the bug

Class A := { a : Type }.
Class B := { ba ::> A }.

(** No coercion! *)
Print Coercions.
Print HintDb typeclass_instances.

Record B' := { ba' ::> A }.

(** Coercion registered as expected. *)
Print Coercions.
Print HintDb typeclass_instances.

Version of Coq where this bug occurs

8.19.1

Last version of Coq where the bug did not occur

No response

[proux01]

Sounds consistent with the fact that ::> means both :: and :>. Will be fixed in 8.21 when the deprecation phase will finally be over. Is it worth changing in 8.20?

[Alizter]

@proux01 Not worth changing I suppose, but I guess you should add this test when the deprecation phase is over. There is also no warning compared to using :> directly in a class.