Existential Datatypes

[Hal Daume III]

I'll take a stab at this:

> data Foo2 = forall a. MkFoo2 { val2 :: a
> 			     , func2 :: a -> Bool
> 			     }
> 
> But the compiler said:
> 
>     Can't combine named fields with locally-quantified type variables
>     In the declaration of data constructor MkFoo2
>     In the data type declaration for `Foo2'

This restriction is probably because having named fields doesn't make too
much sense.  All named fields do is make functions, so:

| data Foo a = Foo { x :: a, y :: a -> Bool }

makes

| data Foo a = Foo a (a -> Bool)

and two functions:

| x :: Foo a -> a
| y :: Foo a -> (a -> Bool)

But in the case of locally quantified type variables, this second part
doesn't make sense.  We know that for the Foo example in the users guide,
we can't write a function:

| func (Foo _ f) = f

because this would allow 'a' to escape.  The same holds here, which is why
(I would imagine) this isn't allowed.

> Then I tried:
> 
> data Foo3 = MkFoo3 { val3 :: forall a. a
> 		   , func3 :: forall a. (a -> Bool)
> 		   }
> 
> foo3 = MkFoo3 'g' isUpper
> 
> And the compiler said:
> 
>     Inferred type is less polymorphic than expected
>         Quantified type variable `a' is unified with `Char'
>     Signature type:     forall a. a
>     Type to generalise: Char
>     When checking an expression type signature
>     In the first argument of `MkFoo3', namely 'g'
>     In the definition of `foo3': MkFoo3 'g' isUpper

This is because the 'a's in the defintion aren't necessarily the same, so
when you say:

  MkFoo3 'g' isUpper

the type of "func3" is Char -> Bool, not a -> Bool, so it's disallowed.

Why this definition is allowed but Foo2 isn't I don't know -- someone else
should chime in there.