29 Jan
2010
29 Jan
'10
5:45 p.m.
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