| Summarizing: without single-field existentially quantified | constructors in newtypes either my code gets less readable or | I have to pay a run-time price. Is it possible to relax the | 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 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 help me out. Corresponding to the types, we have terms to 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: 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 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