[Haskell-cafe] Re: Non-termination of type-checking

[Dan Doel]

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