[Haskell-cafe] Re: Existentials and type var escaping

[Roberto Zunino]

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.