[Haskell] Type problem

[Emil Axelsson]

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
>