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

[Jim Apple]

On 1/15/07, Doaitse Swierstra <doaitse at cs.uu.nl> 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