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