Hello folks A section on GADTs in the GHC user's guide gives a simple example: data Term a where Lit :: Int -> Term Int Succ :: Term Int -> Term Int IsZero :: Term Int -> Term Bool eval :: Term a -> a eval (Lit i) = i eval (Succ t) = 1 + eval t eval (IsZero t) = eval t == 0 let's add Sum :: Term Int -> Term Int -> Term Int eval (Sum l r) = eval l + eval r it's ok But when I do this Sum :: (Num a) => Term a -> Term a -> Term a eval (Sum l r) = eval l + eval r --- same it doesn't typecheck with the error "no isntance Num a" writing eval (Sum (l::Num b => Term b) (r::Num b => Term b)) doesn't help. I wonder, if there's a way to do what I'm trying to do. After all, I'm allowed to declare Term that way. Or is this a restriction of type refinement?