Roberto Zunino wrote:
foo, as defined above does not work (lazy patterns not allowed), and in
foo y = E (case y of E x -> x)
a variable escapes. I also tried with CPS with no success.
Is foo definable at all? I'm starting to think that it is not, and that there must be a very good reason for that...
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. If you make the type argument explicit, you have foo (E <t> x) = E <t> x foo _|_ = E ??? _|_ The ??? can't be a divergent type term, because there aren't any; it must be a type, but no suitable type is available (foo has no type argument). You can't even use some default dummy type like (), even though _|_ does have that type, because you'd have to solve the halting problem to tell when it's safe to default. I'm less clear on how important it is that type terms don't diverge. I think it may be possible to write cast :: a -> b if this restriction is removed, but I don't actually know how to do it. -- Ben