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

[Jonathan Cast]

On Thu, 2009-01-08 at 20:11 +0000, DavidA wrote:
> 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).

> ...

> 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,

It's missing in Haskell 98.  If you add the pragma

{-# LANGUAGE ScopedTypeVariables #-}

then GHC (at least) will accept the variant syntax

inv :: forall n. IntegerAsType n => Fp n -> Fp n

and the definition as you gave it.  Since Haskell 98 doesn't have any
feature like this, GHC can't really introduce it without requiring you
to deviate from Haskell 98 syntax as well :(

jcc