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

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