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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
