[Agda] Universe-Heterogeneous tree

[Philipp Hausmann]

Hi all,

I'm a bit stuck with a problem with the universe levels of Agda.

What I'm trying to do is to create a small AST representing Haskell-like
types in Agda. A
simplified version of my datatype looks like this:

data AST {l} : Set (suc l) where
  -- function type
  _=>_ : AST {l} -> AST {l} -> AST
  -- A concrete named type, e.g. Nat, Int, or also Set
  ty : Set l -> AST

The problem with the above definition is that
all "ty" nodes in the tree need to have the same level.
It's not possible to write e.g. the following:

(ty Set0) => (ty Nat)

"ty Set0" requires the level to be 1, "ty Nat" forces it to be 0. In
this example,
there are only two different levels, but deeper trees may require an
arbitrary number
of different levels, one for each leaf node of the AST.

So what I want is basically a universe heterogeneous tree. What I tried
so far is the following:

1. Index the datatype on a level argument:

data AST ... : (l : Level) -> Set l where
  ....

Agda doesn't accept this: "The sort of AST cannot depend on its indices
...."


2. The Level.Lift record by itself doesn't help, as it does not hide any
Level arguments.

3. Add one additional level argument to AST:

data AST {l m} : Set (sup l m)
  _=>_ : AST {l} {l} -> AST {m} {m} -> AST
  .....

Now the whole tree takes exactly two level arguments instead of one.
This does not solve the problem,
as a tree might require more than two level arguments. E.g.:
  (ty Set0) => (ty Set1) => (ty Set2)




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.


Do you maybe have any ideas or hints?

Philipp