[Agda] Telescope syntax

[Guillaume Brunerie]

Hello all,

As is well known, it’s currently a bit annoying to use universe
polymorphism in Agda because instead of writing

  f : (A B C : Type) -> …

you have to write

  f : {i j k : Level} (A : Set i) (B : Set j) (C : Set k) -> …

Would it be a good idea to make the first one a syntactic sugar for
the second one?
I’m thinking about adding a "telsyntax" keyword, such that you can
write for instance

  telsyntax {i : Level} (X : Set i) = (X : Type)

and then (A B C : Type) (in a telescope) would be automatically translated into

  {i : Level} (A : Set i) {j : Level} (B : Set j) {k : Level} (C : Set k)

And this is not just about universe management, but it would also be
very useful when using instance arguments. For instance if a group is
a type (of level 0, say) with a group structure (which will be found
by instance search), and you want to write a function taking three
groups as arguments you have to write

  g : (G H K : Set) {{_ : GroupStr G}} {{_ : GroupStr H}} {{_ :
GroupStr K}} -> …

But you could say instead

  telsyntax (G : Set) {{_ : GroupStr G}} = (G : Group0)
  g : (G H K : Group0) -> …

And of course you can combine the two, if groups can be at any
universe level then the following:

  telsyntax {i : Level} (G : Set i) {{_ : GroupStr G}} = (G : Group)
  g : (G H K : Group) -> …

would be a shorthand for

  g : {i j k : Level} {G : Set i} {H : Set j} {K : Set k} {{_ :
GroupStr G}} {{_ : GroupStr H}} {{_ : GroupStr K}} -> …

which is much less readable and annoying to write.

One drawback (in the case of universe levels) is that you don’t have
access to the level anymore, but I don’t think that would really be a
problem, and you still can make the levels explicit if you need to.
Another drawback is that when writing (A : Type) or (G : Group) in a
telescope, it makes it look like Type and Group are types, but it’s
not the case so it could be confusing (for instance you can’t end a
function with "-> Group"). If that’s indeed too confusing, maybe we
could use a different notation than a colon, to make it clear that
it’s just syntactic sugar (on the other hand, it looks nice with a
colon).

What do you think?

Guillaume