[Haskell] No fun with phantom types

[Michael Marte]

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