Unspecified universe levels (_) trigger a syntax error in Type with sort variables

[kyoDralliam]

Description of the problem

Not being explicit with universe levels in Type@{s| .. }, e.g. using _ instead of a universe level variable, triggers a syntax error. This is both a usability issue (more annoying to use) and an incompleteness issue because it can be simulated with an auxilliary definition.

Small Coq file to reproduce the bug

Set Universe Polymorphism.
Set Printing Universes.

(* Fully explicit definition: we would like to spare the annotation u *)
Definition id@{s|u|} (A : Type@{s|u}) (a : A) : A := a.


(* Some kind of typical ambiguity can be simulated by rebinding Type to an auxilliary definition T*)
Definition T@{s|u|} := Type@{s|u}.
Definition idT@{s|+|} (A : T@{s|_}) (a : A) : A := a.

(* The actual problem *)
Definition id0@{s|+|} (A : Type@{s|_}) (a : A) : A := a.
(*
Error:
Syntax error: [universe] expected after '|' (in [sort]).
 *)

Version of Coq where this bug occurs

8.19.0

Last version of Coq where the bug did not occur

No response

[Alizter]

What's the difference with writing Type@{q}?

[SkySkimmer]

That will interpret q as a universe not a quality.