RFC: more universe annotations

Stream: lean4

[Arthur Adjedj]

Currently, explicit universes annotations are only allowed when following an identifier. However, this means that explicit annotations do not work on swift dot notation or generalized dot notation:

#check List.cons.{0} [] --works
#check (.cons.{0} []: List Nat) --unexpected token '.{'; expected ')', ',' or ':'
#check [].cons.{0} --unexpected token '.{'; expected command

What this means in practice is that if you work in a setting in which universe unification doesn't behave well, and you need many explicit annotations, you get stripped of the opportunity to use the latter two notations. Is this worth making an RFC ?