Ben Rudiak-Gould wrote:
It's not definable, and there is a good reason. Existential boxes in principle contain an extra field storing their hidden type, and the type language is strongly normalizing.
Thank you very much for the answer: indeed, I suspected strong normalization for types had something to do with that. More in detail, I was actually trying to understand if I could define an infinite list for the following GADT: data List len a where Nil :: List Zero a Cons :: a -> List len a -> List (Succ len) a Here, the len argument fixes the length of the list. So, if len is some fixed type - say the encoding of n - it proves that the list has length n and therefore is finite (although may contain _|_). However, I wondered if this property (finite length) might get invalidated using an existential: data AList a where L :: List len a -> AList a -- translation of: ones = 1 : ones ones :: AList Int ones = L (case ones of L os -> Cons 1 os) but the last line fails to compile. I threw anything at that, but each attempt failed. From your answer, I see that this is indeed impossible. Zun.