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

Emil Axelsson emax at chalmers.se
Wed Sep 9 07:03:46 EDT 2009

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
     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.


/ Emil

More information about the Haskell-Cafe mailing list