[Haskell-cafe] Strange type error (tfp package + GADTs)

[Emil Axelsson]

I forgot to say that I'm using GHC 6.10.1.

Also, the code requires

{-# LANGUAGE FlexibleContexts, GADTs, TypeOperators #-}

/ Emil



Emil Axelsson skrev:
> Hi Café,
> 
> Can anyone explain why `add1` is rejected in the code below (which uses 
> the tfp package):
> 
> 
> 
> import Types.Data.Num
> 
> data A n
>   where
>     A :: NaturalT n => Int -> A n
> 
> getA :: A n -> Int
> getA (A n) = n
> 
> add1 :: NaturalT (m:+:n) => A m -> A n -> A (m:+:n)
> add1 (A a) (A b) = A (a+b)
> 
> add2 :: NaturalT (m:+:n) => A m -> A n -> A (m:+:n)
> add2 a b = A (getA a + getA b)
> 
> add3 :: NaturalT (m:+:n) => A m -> A n -> A (m:+:n)
> add3 (A a) _ = A a
> 
> 
> 
> `add2` and `add3` are accepted. As far as I can see, `add2` is 
> equivalent to `add1` except that it delegates the pattern matching to 
> the function `getA`. If I only pattern match on one of the arguments, as 
> in `add3`, things are also fine.
> 
> Thanks!
> 
> / Emil
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe