Hello *, I am trying to extend the finite-domain (FD) constraint solver proposed by David Overton (http://overtond.blogspot.com/2008/07/pre.html) with arithmetic constraints by means of an embedded DSL. In principle, this is a very natural thing to do in a functional language; it is basically a matter of defining some suitable operators: data FDVar = FDVar Int deriving Show -- the type of FD variables data AExp = --the type of arithmetic expression over FD variables and integers IntegerConstant Int | Variable FDVar | Addition AExp AExp | Subtraction AExp AExp | Multiplication AExp AExp | IntegerDivision AExp AExp deriving Show infixl 7 #* -- multiplication infixl 7 #/ -- integer division infixl 6 #+ -- addition infixl 6 #- -- subtraction (#+), (#-), (#*), (#/) :: (MakeAExp a, MakeAExp b) => a -> b -> AExp (#+) = parseArgs Addition (#-) = parseArgs Subtraction (#*) = parseArgs Multiplication (#/) = parseArgs IntegerDivision with class MakeAExp a where makeAExp :: a -> AExp instance MakeAExp Int where makeAExp = IntegerConstant instance MakeAExp FDVar where makeAExp = Variable instance MakeAExp AExp where makeAExp = id parseArgs :: (MakeAExp a, MakeAExp b) => (AExp -> AExp -> c) -> a -> b -> c parseArgs f x y = f (makeAExp x) (makeAExp y) So far, so good. To avoid that FD variables escape their constraint stores, David employed a phantom type variable s leading to newtype FDVar s = FDVar { unFDVar :: Int } deriving (Ord, Eq) Trying to thread the phantom variable through my DSL implementation, I ended up with the following code: data AExp s = IntegerConstant Int | Variable (FDVar s) | Addition (AExp s) (AExp s) | Subtraction (AExp s) (AExp s) | Multiplication (AExp s) (AExp s) | IntegerDivision (AExp s) (AExp s) class MakeAExp a s where makeAExp :: a -> AExp s instance MakeAExp Int s where makeAExp = IntegerConstant instance MakeAExp (FDVar s) s where makeAExp x = Variable x instance MakeAExp (AExp s) s where makeAExp = id parseArgs :: (MakeAExp a s, MakeAExp b s) => (AExp s -> AExp s -> c s) -> a -> b -> c s parseArgs f x y = f (makeAExp x) (makeAExp y) infixl 7 #* -- multiplication infixl 7 #/ -- integer division infixl 6 #+ -- addition infixl 6 #- -- subtraction (#+), (#-), (#*), (#/) :: (MakeAExp a s, MakeAExp b s) => a -> b -> AExp s (#+) = parseArgs Addition (#-) = parseArgs Subtraction (#*) = parseArgs Multiplication (#/) = parseArgs IntegerDivision This code works if only one operator is applied: *FD> :type let x = (1::Int) in x #+ x let x = (1::Int) in x #+ x :: AExp s but *FD> :type let x = (1::Int) in x #+ x #+ x let x = (1::Int) in x #+ x #+ x :: (MakeAExp (AExp s) s1) => AExp s1 It appears to me that ghci generates two phantom types s and s1 and fails to unify them. Only the extensive use of type constraints seems to help like in the following example, where I used Int as phantom type: *FD> :type ((((1::Int) #+ (1::Int)) :: AExp Int) #+ (2::Int))::AExp Int ((((1::Int) #+ (1::Int)) :: AExp Int) #+ (2::Int))::AExp Int :: AExp Int But this approach only works on the command line and is out of question anyway. Any idea how to make my code work? I am using ghc 6.8.2 with {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} Thanks, Michael