What we claim in our paper is that it's fine to encode universe-polymorphic datatypes using our descriptions, as long as quantification over levels happen outside of the description.
However, currently the deriveDesc macro doesn't do this automatically, which means you cannot derive descriptions for universe-polymorphic datatypes right now.
Two approaches:
- Do as we say in the paper, that is, quantify outside of the description.
- Do as Josh Ko et al (2022) and add levels that are quantified over in the description.
What we claim in our paper is that it's fine to encode universe-polymorphic datatypes using our descriptions, as long as quantification over levels happen outside of the description.
However, currently the
deriveDescmacro doesn't do this automatically, which means you cannot derive descriptions for universe-polymorphic datatypes right now.Two approaches: