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

[Simon Peyton-Jones]

Try the HEAD.  GADTs + type classes are broken in 6.6., and will stay that way I'm afraid.

Simon

| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On Behalf Of Daniil
| Elovkov
| Sent: 22 March 2007 17:12
| To: haskell-cafe at haskell.org
| Subject: [Haskell-cafe] type refinement to a typeclass constrained type
|
| 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?
| _______________________________________________
| Haskell-Cafe mailing list
| Haskell-Cafe at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe