I'm afraid that GHC does not treat the interaction of type classes and GADTs properly. Your example shows this up even more starkly than usual: why should the IsZ thing work, but the Div one not work? The right fix is alas not very simple, which is why I have not done it. (It involves what Martin Sulzmann calls "implication constraints".) However, GADTs and type classes ought to be fine together, and the fact that many people have reported bugs suggests that the interaction is useful. I plan to tackle it in the next couple of months. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of J. Garrett Morris | Sent: 10 October 2005 18:06 | To: glasgow-haskell-users@haskell.org | Subject: GADT question | | Hello, | | 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 | Inc :: Term Int -> Term Int | IsZ :: Num a => Term a -> Term Bool | Div :: Fractional a => Term a -> Term a -> Term a | If :: Term Bool -> Term a -> Term a -> Term a | | and extending the eval function accordingly: | | eval :: Term a -> a | eval (Lit i) = i | eval (Inc t) = eval t + 1 | eval (IsZ t) = eval t == 0 | eval (Div t u) = eval t / eval u | eval (If cond cons alt) = if eval cond then eval cons else eval alt | | I get an error "No instance for (Fractional a) arising from the use of | '/'" This seems odd to me, since Div is constrained to have | fractional arguments. Is there something obvious I'm missing?