Ambiguous type using explicit quantifiers

Question

Minimal example code:

class IntegralAsType a where
  value :: (Integral b) => a -> b

class (Num a, Fractional a, IntegralAsType q) => Zq q a | a -> q where
  changeBase:: forall p b . (Zq q a, Zq p b) => a -> b

newtype (IntegralAsType q, Integral a) => ZqBasic q a = ZqBasic a deriving (Eq)

zqBasic :: forall q a . (IntegralAsType q, Integral a) => a -> ZqBasic q a
zqBasic x = ZqBasic (mod x (value (undefined::q)))

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase (ZqBasic x) = fromIntegral (value (undefined::p)) -- ZqBasic is an instance of Num

Here's a little background on what I'm trying to accomplish: IntegralAsType ensures type safety at compile time by preventing something like addition of two numbers with different modulus. ZqBasic is an internal representation of the Zq type, there are others, which is why Zq is defined the way it is. The goal is to get a system that is transparent to the internal representation.

My problem is with the changeBase function. I'm using explicit forall on the 'p' type, but I still get an "ambiguous type variable a0 in the constraint (IntegralAsType a0) arising from the use of value"

I'm confused on why I'm getting this error. In particular in a previous post, I got help with something like the "zqBasic" function, which appears to have the same setup as the changeBase function. I fixed the ambiguous variable error in zqBasic by adding the explicit quantifier 'forall q a .' Without this quantifier, I get an ambiguous type variable error. I understand why I need the quantifier there, but I don't understand why it doesn't seem to be helping for changeBase.

Thanks

Answer 1

Two (essentially equivalent?) approaches that work:

1: Using C.A. McCann's approach:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase (ZqBasic x) = b
    where b = fromIntegral ((value (zq b))*(fromIntegral (value (zq q)))) -- note that 'q' IS in scope

2: Rather than having the signature a->b, I changed the signature of changeBase to b->a The following then works:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase x = fromIntegral ((value (zq x))*(fromIntegral (value (zq q)))) -- note that 'q' IS in scope

The goal was always to be able to access the type parameters for both the argument and return type, and both of these approaches allow me to do that.

Also, the answer to my question about the difference between the 'zqBasic' constructor and 'changeBase' is, as C.A.McAnn indicated, that 'p' was not put into scope in declarations, even with an explicit forall. If anyone can explain why this is, I'd appreciate it.

Answer 2

Using ScopedTypeVariables isn't helping here because the p you're using isn't in scope anyway, it seems. Compare the following definitions:

changeBase (ZqBasic x) = fromIntegral (value (undefined::foobar))

This gives the same error, because it's also creating a new type variable.

changeBase (ZqBasic x) = fromIntegral (value (5::p))

This, however, gives a different error. The relevant bits are:

Could not deduce (Num p1) arising from the literal `5'
        (snip)
    or from (Zq q (ZqBasic q a), Zq p b)
      bound by the type signature for
                 changeBase :: (Zq q (ZqBasic q a), Zq p b) => ZqBasic q a -> b

This shows that p is being instantiated as a fresh type variable. I'm guessing that the forall on the type signature doesn't bring into scope (in actual declarations) the type variables that aren't the class's type parameters. It does bring the variable into scope for a default declaration, however.

Anyway, that's neither here nor there.

It's easy enough to work around most problems with needing access to type variables--just create some auxiliary functions that don't do anything but let you manipulate the types appropriately. For instance, a nonsense function like this will pretend to conjure up a term with the phantom type:

zq :: (Zq q a) => a -> q
zq _ = undefined

This is basically just giving you direct term-level access to the functional dependency, since the fundep makes q unambiguous for any particular a. You can't get an actual value, of course, but that's not the point. If the undefined bothers you, use [] :: [q] instead to similar effect and use head or whatever only when you need to.

Now you can twist things around a bit using a where clause or whatnot to forcibly infer the correct types:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase (ZqBasic x) = b
    where b = fromIntegral (value (zq b))

What's going on here is that b is the actual thing we want, but we need value to see the type p which is determined by the type of b, so by assigning a temporary name to the result we can use that to get the type we need.

In many cases you could also do this without the extra definition, but with type classes you need to avoid the ad-hoc polymorphism and ensure it doesn't allow the "recursion" to involve other instances.

On a related note, the standard library function asTypeOf is for exactly this type of fiddling with types.

Answer 3

The call value (undefined::p) converts from p to some type a0. From the type of value, the only thing we can figure out is that a0 is an integral type.

That value is passed to fromIntegral, which converts from a0 to b. From the type of fromIntegral, the only thing we can figure out is that a0 is an integral type.

Nothing determines what type a0 is, so a type annotation is needed on the expression value (undefined::p) to resolve the ambiguity. From looking at your type signatures, it looks like value should be able to generate the correct return type without doing any extra conversions. Can you simply remove the call to fromIntegral?

Edit

You need to enable the ScopedTypeVariables extension. Without ScopedTypeVariables, a type variable cannot be mentioned in more than one type signature. In this case, the variable name p does not refer to the same variable in the function's type signature and in its body.

The following code works for me:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase = zqBasicChangeBase

zqBasicChangeBase :: forall p b q a.
  (IntegralAsType q, IntegralAsType p, Integral a, Zq p b) => ZqBasic q a -> b
zqBasicChangeBase (ZqBasic x) = fromIntegral (value (undefined :: p) :: Integer)