[Haskell-cafe] Re: Non-termination of type-checking
dan.doel at gmail.com
Fri Jan 29 17:45:16 EST 2010
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.
More information about the Haskell-Cafe