Hi, I've been told the following short code is correct but it's GHC's fault it does not type check. Is that the case? -- {-# OPTIONS -fglasgow-exts #-} -- An expression GADT: data Exp :: * -> * where LitNum :: Num a => a -> Exp a LitBool :: Bool -> Exp Bool Plus :: Num a => Exp a -> Exp a -> Exp a And :: Exp Bool -> Exp Bool -> Exp Bool If :: Exp Bool -> Exp a -> Exp a -> Exp a -- An expression evaluator: evalExp :: Exp a -> a evalExp (LitNum i) = i evalExp (LitBool b) = b evalExp (Plus x y) = evalExp x + evalExp y evalExp (And x y) = evalExp x && evalExp y evalExp (If c t e) = if (evalExp c) then (evalExp t) else (evalExp e) -- The type checker complains that evalExp needs a Num constraint on its type signature. This can't be right, for Bool is not an instance of Num, right? Is it the case that the interaction between GADTs and type classes is not fully worked out yet? Here is a related problem. I'd like to make the types of expressions extensible by using a type class: -- class TyRange a instance TyRange Int instance TyRange Bool data Exp :: * -> * where Lit :: TyRange a => a -> Exp a Plus :: Exp Int -> Exp Int -> Exp Int And :: Exp Bool -> Exp Bool -> Exp Bool If :: TyRange a => Exp Bool -> Exp a -> Exp a -> Exp a But I cannot add the types in other classes into TyRange in modular fashion, cause the superclass is specified at the moment of declaration. I may try to extend TyRange by adding the instances in, say, Num: -- {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} class TyRange a instance TyRange Bool instance Num a => TyRange a data Exp :: * -> * where Lit :: TyRange a => a -> Exp a Plus :: Exp Int -> Exp Int -> Exp Int And :: Exp Bool -> Exp Bool -> Exp Bool If :: TyRange a => Exp Bool -> Exp a -> Exp a -> Exp a evalExp :: Exp a -> a evalExp (Lit i) = i evalExp (Plus x y) = evalExp x + evalExp y evalExp (And x y) = evalExp x && evalExp y evalExp (If c t e) = if (evalExp c) then (evalExp t) else (evalExp e) -- But I get the following error when evaluating evalExp (If (Lit True) (Lit 1) (Lit 2)) Overlapping instances for TyRange Bool arising from use of `Lit' at <interactive>:1:13-15 Matching instances: /home/pni/Papers/EDT/TyRangeProblem.hs:5:0: instance TyRange Bool /home/pni/Papers/EDT/TyRangeProblem.hs:4:0: instance (Num a) => TyRange a In the first argument of `If', namely `(Lit True)' In the first argument of `evalExp', namely `(If (Lit True) (Lit 1) (Lit 2)) Apologies for being so daft, but why are the instances overlapping if Bool is not in Num?