[Haskell-cafe] type refinement to a typeclass constrained type

[Daniil Elovkov]

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?