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

Jim Apple wrote in article in gmane.comp.lang.haskell.cafe:

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?

I consider it a foundational reason. You seem to want (forall (f :: * -> *) . f) to have kind * -> *. But that means that I should be able to apply it to a type, say Int, to get a type (forall (f :: * -> *) . f) Int. What values inhabit this type? -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig My mother is a fish.