{-# 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