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

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

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)

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

Anatoly Yakovenko