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

Anatoly Yakovenko aeyakovenko at gmail.com
Mon Sep 22 23:10:44 EDT 2008

> 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:

    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)

More information about the Haskell-Cafe mailing list