[Haskell-cafe] "Inconsistency" in support for phantom types?

[DavidA]

Hi,

I have run into what appears to be an inconsistency in the support for using
phantom types to parameterize other types. Here's an example (don't pay too much
attention to the maths, it's just there to motivate the example). I want to
define types for the finite fields with 2, 3 and 5 elements (clock arithmetic
modulo 2, 3 or 5).

{-# OPTIONS_GHC -fglasgow-exts #-}

class IntegerAsType a where
    value :: a -> Integer

-- three phantom types:
data T2
instance IntegerAsType T2 where value _ = 2
data T3
instance IntegerAsType T3 where value _ = 3
data T5
instance IntegerAsType T5 where value _ = 5

newtype Fp n = Fp Integer deriving (Eq,Ord)

-- our three finite field types:
type F2 = Fp T2
type F3 = Fp T3
type F5 = Fp T5

-- Show and Num instances
instance Show (Fp n) where
    show (Fp x) = show x

instance IntegerAsType n => Num (Fp n) where
    Fp x + Fp y = Fp $ (x+y) `mod` value (undefined :: n)
    negate (Fp 0) = 0
    negate (Fp x) = Fp $ value (undefined :: n) - x
    Fp x * Fp y = Fp $ (x*y) `mod` value (undefined :: n)
    fromInteger m = Fp $ m `mod` value (undefined :: n)

Now, we can also define a Fractional instance, using the extended Euclid
algorithm (given at the end)

-- n must be prime
instance IntegerAsType n => Fractional (Fp n) where
    recip 0 = error "Fp.recip 0"
    recip (Fp x) = let p = value (undefined :: n)
                       (u,v,1) = extendedEuclid x p
                       -- so ux+vp = 1. (We know the gcd is 1 as p prime)
                   in Fp $ u `mod` p

Now, the problem I've run into is, what do I do if I want to define a function
parameterised over the phantom types, but without doing it as part of a type
class instance? For example, suppose that I had just wanted to define "inv" as a
synonym for "recip":

inv :: IntegerAsType n => Fp n -> Fp n
inv 0 = error "Fp,inv 0"
inv (Fp x) = let p = value (undefined :: n)
                 (u,v,1) = extendedEuclid x p
             in Fp $ u `mod` p

"inv" has exactly the same code as "recip", but now the IntegerAsType constraint
is part of the type signature, rather than an instance constraint. It seems that
this means that the constraint is not available to the code during compilation,
because when I try to compile this I get
    Ambiguous type variable `n' in the constraint:
      `IntegerAsType n' arising from a use of `value' at Test.hs:52:21-42
    Probable fix: add a type signature that fixes these type variable(s)

It seems to me highly desirable that this code should compile as expected, just
as the recip code compiles. Is it a bug in GHC, or a missing language feature,
or is there a "better" way to do what I'm trying to do?

Thanks, David

-- extendedEuclid a b returns (u,v,d) such that u*a + v*b = d
extendedEuclid a b | a >= 0 && b >= 0 = extendedEuclid' a b [] where
    extendedEuclid' d 0 qs = let (u,v) = unwind 1 0 qs in (u,v,d)
    extendedEuclid' a b qs = let (q,r) = quotRem a b in extendedEuclid' b r (q:qs)
    unwind u v [] = (u,v)
    unwind u v (q:qs) = unwind v (u-v*q) qs