On 1/15/07, Doaitse Swierstra <[EMAIL PROTECTED]> 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
