[atennapel]

I'm not sure what you mean with totally expanded type space. But it sounds like Dhall has an issue with unfolding/normalisation.

Totality shouldn't have any special impact on memory usage as far as I know. It just restricts the kind of recursive functions and data types you can write.

[solatic]

If you have a sum type `< a : A | b : B | c : C >.a`, then A, B, and C need to be unfolded. If A itself is of type `< j : J | k : K | l : L >`, and J is also a sum type, etc., then unfolding everything can result in exponential memory usage and exhaust the amount of available memory. Of course there are ridiculously high-memory systems available, but then it's no longer economical.