[Agda] Universe-Heterogeneous tree

[effectfully]

Hi.

In the `ast` function `ls' can be always inferred, when `T' is
provided, because `AST' is constructor-headed. And in the other
direction: `T' can be inferred, when the spine of `ls' is provided
like this:

example : ast (ty _ => ty _) _
example = 3 , (ℕ × ℕ)

However Agda can't infer both, because `ast' is not
constructor-headed. But you can make it:

record Leaf {α} (A : Set α) : Set α where
  constructor leaf
  field unleaf : A

ast : {ls : ASTLevel} {T : AST ls} → Set (bound ls)
ast {ls => ms} {T , U} = ast {T = T} × ast {T = U}
ast {ty l}     {T}     = Leaf T

Now these universe polymorphic trees look more tree-like and you also
don't need to supply additional type information just like with usual
trees:

example : ast
example = leaf 3 , leaf (ℕ × ℕ)

> So I'm kind of unsure what else to try. I suspect it may be possible to
> do this by avoiding datatypes and
> just using functions, but I haven't investigated this yet and I'm trying
> to avoid going in that direction.

The solution, gallais gave you, uses functions, but it's pretty
unproblematic. You will need to pattern match on `ASTLevel' to be able
to pattern match on `ast', and you will need to compute levels
recursively in return types of some functions, but this is
straightforward. I doubt there is a better solution.