Re: newtype and existentials

On Fri, Nov 18, 2005 at 02:28:28PM +0100, Ralf Hinze wrote:
> Is there a strong reason why
> 
> > {-# OPTIONS -fglasgow-exts #-}
> > data Type :: (* -> *) where
> >   Int   ::  Type Int
> > data Dynamic  =  forall a . Dyn (a, Type a)
> 
> works, but not
> 
> > newtype Dynamic  =  forall a . Dyn (a, Type a)

I am not an expert in this area, but let's try to guess.

My guess is that there is no strong reason and the rule that
existentials can be only used in 'data' declarations is a bit
too restrictive. Usually, you restrict the existentially
quantified types to some type-classes. This requires storing
the type-class dictionaries in the data constructor, which
changes the representation of the type, so newtype can't be
used.

In your case you don't use type-class context to restrict 'a',
so it should be possible to use newtype. But the compiler
is not so smart to see this and it rejects this code anyway.

Did I win something? ;-)

Best regards
Tomasz