On 1/15/07, Doaitse Swierstra wrote:

Values that live as elements in data have to be data themselves, and thus have to be of a type that has kind *.

But the example I give doesn't have a "value" of kind * -> * living in data. The constructor is nullary, only the parameter to the type is not of kind *. This is fine in declarations like: data Good (x :: * -> *) where Good :: Good Maybe What I'm asking is why, for declarations like data OK (x :: * -> *) where OK :: OK x type Fine = OK Maybe type Evil = OK (forall (f :: * -> *) . f) Fine is allowed, while Evil is not. This is not the case for data OK' (x :: *) where OK' :: OK' x type Fine' = OK' Maybe type Evil' = OK' (forall (f :: *) . f) When both Fine' and Evil' are accpeted. Jim

On Jan 15, 2007, at 3:39 AM, Jim Apple wrote:

...

Why is this declaration ill-formed:

data Bad t where Bad :: Bad (forall (f :: * -> *) . f)

GHC 6.6 says:

`f' is not applied to enough type arguments Expected kind `*', but `f' has kind `* -> *' In the type `forall f :: (* -> *). f' In the type `Bad (forall f :: (* -> *). f)' In the data type declaration for `Bad'

I suppose this is because the kind inference rule is

C, x : k1 |- y : * ----------------------- C |- (\forall x : k1 . y) : *

I'd expect

C, x : k1 |- y : k2 ----------------------- C |- (\forall x : k1 . y) : k2

Is there a foundational or an implementation reason for this restriction?

Jim