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

Jim Apple jbapple+haskell-cafe at gmail.com
Sun Jan 14 21:39:42 EST 2007


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


More information about the Haskell-Cafe mailing list