> 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)
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
