Cannot declare global typeclass field in definitional class

[rlepigre]

Description of the problem

The following code:

Class Junk.

Class Dummy : Type :=
  something :> Junk.

produces the warning:

Warning: A coercion will be introduced instead of an instance in future versions when using ':>' in 'Class'
declarations. Replace ':>' with '::' (or use '#[global] Existing Instance field.' for compatibility with Coq <
8.17). Beware that the default locality for '::' is #[export], as opposed to #[global] for ':>' currently. Add an
explicit #[global] attribute to the field if you need to keep the current behavior. For example: "Class foo := {
#[global] field :: bar }." [future-coercion-class-field,records]

However, there is no way to use the syntax:

Class Dummy : Type :=
  #[global] something :: Junk.

It works without the #[global] but the something instance is then export. Of course, the other workaround with Existing Instance works, but the warning is confusing since there is no record here.

Coq Version

8.17.0

cc @Janno

[Blaisorblade]

Since this is new with #16230, tagging @proux01 (and including the same labels as the MR).

[proux01]

The best solution would be to add support for locality attribute to the "single field" of definitional typeclasses, but that's non trivial and I don't have time to do that right now. So let's at least fix the confusing warning message: #17485