[Haskell-cafe] existential types (was Re: Optimization problem)

On Thu, Sep 28, 2006 at 03:22:25PM +0100, Simon Peyton-Jones wrote:

| Does anything go wrong with irrefutable patterns for existential types?

Try giving the translation into System F.

I'm a bit puzzled about this. A declaration data Foo = forall a. MkFoo a (a -> Bool) is equivalent to newtype Foo = forall a. Foo (Foo' a) data Foo' a = MkFoo a (a -> Bool) except that you also don't allow existentials with newtypes, for similarly unclear reasons. If you did allow them, you'd certainly allow this equivalent of the original irrefutable match: ... case x of Foo y -> let MkFoo val fn = y in fn val So, is there some real issue with existentials and non-termination?