Try n01 :: Nat One
-- ryan On Mon, Sep 22, 2008 at 8:10 PM, Anatoly Yakovenko <[EMAIL PROTECTED]> wrote: >> 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 > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
