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
