[Haskell-cafe] Re: having fun with GADT's

[Anatoly Yakovenko]

> type One = S Z
> type Two = S One
> etc.

why does:

data Nat a where
   Z :: Nat a
   S :: Nat a -> Nat (S a)

data Z
data S a

type One = S Z
n00 = Z
n01::One = S n00

give me:

test.hs:10:11:
    Couldn't match expected type `One'
           against inferred type `Nat (S a)'
    In the expression: S n00
    In a pattern binding: n01 :: One = S n00
Failed, modules loaded: none.


or better yet, how is type S Z different from, n01 :: forall a. Nat (S a)