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.