Hi Garret, As others have mentioned, this is currently not supported, but it seems that it will be at some point. On the sf bug-tracker, I could find the following entries, but the issue has also been discussed on the mailing list. http://sourceforge.net/tracker/index.php?func=detail&aid=1116210&group_id=8032&atid=108032 http://sourceforge.net/tracker/index.php?func=detail&aid=1180651&group_id=8032&atid=108032 Interestingly, unlike in the constrained-datatype-case, ghc's run-time representation of constrained gadts contains the dictionary, but there is no way to access it (well, except unsafeCoerce#) that I am aware of. So, how can we fake the desired behavior? Existential quantification allows us to store and access a dictionary, and we can witness type equality using GADTs, as in the E datatype below. Notice that Fractional b => f b can be expressed as exists a. (Fractional a) and (a = b) => f b Therefore, the following dataype is equivalent to yours and eval can be implemented on top of it. data E :: * -> * -> * where E :: E a a data Term :: * -> * where Lit :: a -> Term a Div :: Fractional a => E a b -> Term a -> Term a -> Term b eval :: Term a -> a eval (Lit i) = i eval (Div e t u) = let q = eval t / eval u in case e of E -> q The case for Div is a little awkward, as ghc needs to be forced to unify type variables and resolve constraints in a specific order for the trick to work. Regards, Thomas On Mon, 2005-10-10 at 13:06 -0400, J. Garrett Morris wrote:
I've been attempting to use GADTs to create a small domain specific language, and I'm running into an odd problem. Adding one case to the example at the beginning of the Wobbly types paper:
data Term :: * -> * where Lit :: a -> Term a Div :: Fractional a => Term a -> Term a -> Term a
and extending the eval function accordingly:
eval :: Term a -> a eval (Lit i) = i eval (Div t u) = eval t / eval u