Existentials and newtype

[Arthur Baars]

At glasgow-haskell-bugs@haskell.org I asked the following:

> this works
>
>        data Exists f = forall x . E ( f  x)
>
> this doesn't work
>
>         newtype Exists f = forall x . E ( f  x)
>
> Hugs accepts both.
>
> It there a reason why existential quantification does not work with a
> newtype, or is it just
> a parser problem?

This problem is clearly not a bug but a restriction imposed by the designers
of GHC,
as Keith Wansbrough pointed out to me:

> >From the manual, section 7.12.3 "Restrictions":
>
> --8<--
> You can't use existential quantification for newtype declarations. So this
is illegal:
>           newtype T = forall a. Ord a => MkT a
>
> Reason: a value of type T must be represented as a pair of a
> dictionary for Ord t and a value of type t. That contradicts the idea
> that newtype should have no concrete representation. You can get just
> the same efficiency and effect by using data instead of newtype. If
> there is no overloading involved, then there is more of a case for
> allowing an existentially-quantified newtype, because the data because
> the data version does carry an implementation cost, but single-field
> existentially quantified constructors aren't much use. So the simple
> restriction (no existential stuff on newtype) stands, unless there are
> convincing reasons to change it.
> --8<--

I perfectly understand why the use of class constraints in combination with
newtype and existential quantification is
illegal. In my opinion the restriction should only forbit this particular
combination, instead of all uses of newtype with existentials.

For me single-field existentially quantified constructors are quite useful:

For example

newtype Exists f = forall x . E (f x)

data Object a = Object {value :: a , toString:: a -> String }

data Thing a = Thing {val :: a , next :: a -> a,  run :: a -> IO ()}

-- Here I hide the type variables of Object and Thing using the type Exists:

type EObject  = Exists Object
type EThing    = Exists Thing

without single-field existentially quantified constructors I would have to
write:

data EObject =  forall  a . EObject a (a -> String)
data EThing   =  forall a . EThing  a  (a -> a)  (a-> IO ())

or write the Exists type using data

When using data I have to pay a (however small) run-time cost, that I would
not have to pay
when using a newtype.

The other solution does not have this run-time cost, but it makes my code
less readable:
I have to invent new types and constructor names.
I cannot use named fields.
I cannot reuse polymorphic functions that work on Object on EObjects.

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?

Cheers, Arthur