On Friday 29 January 2010 5:26:28 pm Matthieu Sozeau wrote:
> data R (c :: *) where
> R :: forall c' :: * -> *, (c' (c' ()) -> False) -> R (c' ()).
This is what the data declaration is. The c on the first line and the c on the
second line are unrelated. It's sort of an oddity of GADT declarations;
variables used between the 'data' and 'where' are just placeholders. With
KindSignatures enabled, one could also write:
data R :: * -> * where
R :: (c (c ()) -> False) -> R (c ())
or explicitly quantify c in the constructor's type.
That confused me at first, as well.
-- Dan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
