Emil Axelsson emax at cs.chalmers.se
Tue Dec 13 04:58:12 EST 2005

```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
>
```