Existentials and newtype

[Simon Peyton-Jones]

| Summarizing: without single-field existentially quantified=20
| constructors in newtypes either my code gets less readable or=20
| I have to pay a run-time price.  Is it possible to relax the=20
| restriction on newtypes in combination with existentials?

Yes, that's a fair point.

Unfortunately, newtype existentials are tricky in GHC, because
GHC's intermediate language is strongly typed.  At the=20
moment, existentials show up in that intermediate language
solely mediated through data constructors.    Newtypes
have gone away by the time we are in the intermediate language.
So there's nowhere to 'hang' the existential for a newtype.

Would be easy to add existentials to the intermediate language?
Unfortunately, not very, unless I misunderstand and someone can=20
help me out.  Corresponding to the types, we have terms to=20
introduce and elminate the type:

Forall type
	Big lambda e.g.   /\a. \x::a -> e
	Type application e.g.  f Int 4

Existential type
	what?

Well, it's well understood what you need for existentials:=20
a sort of pair for introduction and a sort of case for elimination.

But I am deeply reluctant to add two new constructors to the Core
language data type, which only has 8 constructors right now,
and which deals quite happily with data-constructor-mediated
existentials.  Adding extra forms of Core would complicate every
single compiler pass.


I've written at some length because I want first class existentials too;
see the paper that Mark and I wrote
=09
http://research.microsoft.com/~simonpj/papers/first-class-modules

But I'm a bit stuck at the moment about how to slip them into
Core without making a big heap of work.

Simon