[Haskell-cafe] Higher kinds (and impredicativity?)

[Jim Apple]

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