[Agda] Size Issue when Modelling Effectful Data Structures and Computations

[jonas.hoefer at stud.htwk-leipzig.de]

Hello,

I have a problem involving universe levels.

I'm trying to implement scoped effects (based on "Effect Handlers in Scope"
by Wu et al.) in Agda. I follow the the higher order approach from the paper.
It models effects using a free monad over a higher order functor.

The approach leads to a tree structure with an existential type in
(potential) every node. I would like to store special data types which use
the tree type itself in the existential type variable, but this obviously
leads to size issues. I have outlined the problem and some ideas in the
following gist. It contains a minimal example of the structure and a larger
example for context.

https://gist.github.com/JonasHoefer/f0a61744b1cb9cf1f649cfe3bcf414bb

I'm not sure how to proceed at this point. Are there any standard approaches
to deal with or transform this kind of size issues?
Storing arbitrary types of the same level is of course not possible, but I'm
dealing with just a limited set of "too large" data types (i.e. just those
which continue the tree). This is not witnessed by the implementation but I
don't know how to use this fact.
Would it be possible (and practical) to work with always increasing universe
levels?

Thanks,
Jonas