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

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