That's good enough until GHC 6.6. Thank you very much! / Emil Tomasz Zielonka skrev:
On Tue, Dec 13, 2005 at 09:46:31AM +0100, Emil Axelsson wrote:
Is this just a limitation of the current GATDs, or is it unreasonable of me to expect this to work?
AFAIK it is a current limitation of GADTs, which will be removed in GHC 6.6.
Is there any workaround, such as coercing the type of the value function?
I've had the same problem myself. The workaround is to replace some of type-class constraints with "witness" GADTs. The code I attached shows how you can do it. I chose to make HasX a GADT, and introduce the HasX' type-class, but the latter is only for convenience. Note the subtle change in Val's definition:
data Val a where ... X :: HasX a -> Val a -- Unconstrained ^^
Best regards Tomasz
------------------------------------------------------------------------
{-# OPTIONS -fglasgow-exts #-}
data Number = XN -- Unconstrained | N Int -- Constrained
data HasX a where HasX_Number :: HasX Number
xVal :: HasX a -> a xVal HasX_Number = XN
class HasX' a where hasX :: HasX a
instance HasX' Number where hasX = HasX_Number
x :: HasX' a => Val a x = X hasX
data Val a where P :: a -> Val a -- Primitive
T2 :: (Val a1, Val a2) -> Val (a1,a2)
X :: HasX a -> Val a -- Unconstrained
value :: Val a -> a value (X hx) = xVal hx value (P a) = a value (T2 (a1,a2)) = (value a1, value a2)
ex1 :: Val (Number,(Number,Number)) ex1 = T2 (P (N 3), T2 (x, P (N 5)))
-- ex2 :: Val (Number,Number) -- ex2 = X