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

[Ryan Ingram]

Try

n01 :: Nat One

  -- ryan

On Mon, Sep 22, 2008 at 8:10 PM, Anatoly Yakovenko
<aeyakovenko at gmail.com> 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
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>