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

[Ross Paterson]

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?