[Agda] Universe-Heterogeneous tree

[effectfully]

It's more convenient to make the second argument of `ast' explicit and
then define an implicit version:

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

astᵢ = λ {ls} {T : AST ls} -> ast T

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

I wonder if it could be implemented in Agda that pattern matching on
constructor-headed functions would not require pattern matching on
their arguments. Then we could write

AST : (ls : ASTLevel) → Set (suc (bound ls))
AST (t => u) = AST t × AST u
AST (ty l)   = Leaf (Set l)

ast : {ls : ASTLevel} (T : AST ls) → Set (bound ls)
ast (T , U)  = ast T × ast U
ast (leaf T) = Leaf T

But this is not very useful feature probably.