1-field-record Typeclass syntax does not support implicit parameters

[RalfJung]

Description of the problem

This code works:

Class MRet (M : Type -> Type) := mret A: A -> M A.

but this one does not:

Class MRet (M : Type -> Type) := mret {A}: A -> M A.

That is quite surprising, given that usually {...} works whenever one defines a sequence of binders.

We currently use this as a work-around:

Class MRet (M : Type -> Type) := mret: forall {A}, A -> M A.

Coq Version

8.13.2

[SkySkimmer]

It's getting confused with the record syntax.
You see, Class foo := bla : t parses like a 1-constructor inductive.
but with the { the parser thinks it's parsing a record constructor and does not backtrack.
You can workaround by adding a |: Class MRet (M : Type -> Type) := | mret A: A -> M A.

Not sure if it's possible to fix this, cc @coq/parsing-maintainers

[SkySkimmer]

The only way to find out that something like Class MRet (M : Type -> Type) := mret {A:Type} : A -> M A. isn't a record with field A is to be ambiguous until the : so definitely seems hard to fix.

[RalfJung]

Ah indeed, this works:

Class MRet (M : Type -> Type) := | mret {A}: A -> M A.

Interesting.