[design] new syntax for declaring fields as existing instances

[Alizter]

Today we can do :> to declare an existing instance in a class. This is confusing for newcomers and makes handling record/class syntax more complicated. Therefore it was deprecated in #15802. The alternative there is to using Existing Instance. Whilst this is fine from a semantic standpoint, it would be nice to introduce some syntactic sugar for doing this at the field level. Another thing is that we don't only have to support classes, but records also.

Here is a proposal:

Record Foo := {
  my_data : My_type ;
  my_instance :: My_class ;
}.

This would do the equivalent of:

Record Foo := {
  my_data : My_type ;
  my_instance : My_class ;
}.
Existing Instance my_instance.

Furthermore we could add an attribute to this field, similarly how the :> in a field can have coercion attributes.

Record Foo := {
  my_data : My_type ;
  #[priority = 20]
  my_instance :: My_class ;
}.

Which would do:

Record Foo := {
  my_data : My_type ;
  my_instance : My_class ;
}.
Existing Instance my_instance | 20.

Other attributes could also be added that govern the mode of the input class (if it is happening inside a class) etc.

The :: syntax is a nod to Haskell which inspired the typeclass mechanism in Coq. I think our parser should be able to support it, though I haven't tried. Other alternative's include :$ where $ can be replaced by any ASCII char we settle on.

I believe that we should provide some syntactic sugar before fully removing :> to mean existing instance today.

cc @RalfJung @Blaisorblade @SkySkimmer @proux01

[RalfJung]

This gives precedence to the :> usecase for coercions over its usecase for instances. My personal preference would be for :> to mean "only instance" and use some other syntax for "only coercion". At least for the code I maintain, that would lead to much less churn -- but this of course depends heavily on the style of one's codebase.

But in the end, I do not care that strongly, as long as there is a transition plan where we only have to change everything once, and we can get Coq's help for the transition: first add the new syntax, then add a warning for the old syntax in the cases where its behavior will change and a way to automatically adjust all uses of the old syntax to the new one that will maintain the desired behavior.

[proux01]

This gives precedence to the :> usecase for coercions over its usecase for instances.

Note that this is just the historic order. :> was used for making fields of records coercions before getting its special meaning when typeclasses were introduced.

[Blaisorblade]

This plan makes sense to me; it's not clear how useful :: is in a non-typeclass record, but supporting the syntax there too is more orthogonal.