ambiguous type variable problem when using forall, multiparameter type classes, and constraints on polymorphic values (and syb-with-class)
Hello, I am trying to understand why I am getting an ambigious type variable error, and what I can do to work around it. The problem is occurring while trying to use syb-with-class, but I have stripped it down to it's bare essentials, so the following code is self-contained, and does not require an understanding of syb-with-class.
{-# LANGUAGE RankNTypes, KindSignatures, MultiParamTypeClasses, FlexibleInstances, ScopedTypeVariables, FlexibleContexts #-} module Main where
A Proxy data type used to pass some extra type info around in gmapQ.
data Proxy (a :: * -> *) = Proxy
A simple multiple parameter type class.
class Data (ctx :: * -> *) a
gmapQ takes a function, forall a. (Data ctx a) => a -> r, applies the function to all the immediate sub-types of 'a' and collects the results as a list. This is possible because the 'a' is forall'd, and (in the real implementation) the Data class provides the mechanisms for accessing all the immediate sub-types of 'a' and doing useful things with them.
gmapQ :: Proxy ctx -> (forall a. (Data ctx a) => a -> r) -> (forall a. (Data ctx a) => a -> [r]) gmapQ = undefined
Now we create a context.
data Foo m a = Foo { unFoo :: m a }
And create a Data instance for it.
instance Data (Foo m) a
Here is an example that attempts to recursively apply itself to all the subtrees. (I believe this function will ultimately return 0, since it tries to sum the results of the children. When you reach types with no more sub-types, I think you will get an empty list, and sum [] == 0. Though it's not really important to the issue at hand).
bar1 :: forall a m r. (Data (Foo m) a, Num r) => a -> r bar1 x = sum $ gmapQ (undefined :: Proxy (Foo m)) bar1 x
The problem I have is when I try to add an additional constraint on 'm', such as (Monad m) =>
-- bar2 :: forall a m r. (Monad m, Data (Foo m) a, Num r) => a -> r -- bar2 x = sum $ gmapQ (undefined :: Proxy (Foo m)) (bar2 :: forall b. (Monad m, Data (Foo m) b, Num r) => b -> r) x
I get the error: /tmp/a.lhs:48:54: Ambiguous type variable `m' in the constraint: `Monad m' arising from a use of `bar2' at /tmp/a.lhs:48:54-57 Probable fix: add a type signature that fixes these type variable(s) Failed, modules loaded: none. Adding all the scoped type variable stuff does not seem to help. Alas, I can not figure out if this is a limitation of the type-checker, or something that is fundamentally impossible. Nor can I figure out how to work around the issue. In my real code I need to define the data instance like:
-- instance (Monad m) => Data (Foo m) a
Which, by itself is fine. But that results in my needing to add (Monad m) to the 'bar' function. And that is what I can't figure out how to do.. Thanks! - jeremy
On Fri, May 21, 2010 at 12:30 PM, Jeremy Shaw
Adding all the scoped type variable stuff does not seem to help. Alas, I can not figure out if this is a limitation of the type-checker, or something that is fundamentally impossible. Nor can I figure out how to work around the issue.
It's either one, depending on how you look at. To explain:
The problem I have is when I try to add an additional constraint on 'm', such as (Monad m) =>
-- bar2 :: forall a m r. (Monad m, Data (Foo m) a, Num r) => a -> r -- bar2 x = sum $ gmapQ (undefined :: Proxy (Foo m)) (bar2 :: forall b. (Monad m, Data (Foo m) b, Num r) => b -> r) x
How might the compiler decide what specific "m" is meant when this function is called, so that it can make sure that it's always a Monad? All it has to work with are "a" and "r". The only connection to "m" is via the Data instance, but the second parameter to Data alone is not really sufficient to find a specific instance--in fact, there could well be multiple such instances.
bar1 :: forall a m r. (Data (Foo m) a, Num r) => a -> r bar1 x = sum $ gmapQ (undefined :: Proxy (Foo m)) bar1 x
Note that "m" is actually ambiguous here as well, but GHC won't complain until it needs to care about the specific type. If everything looks fully polymorphic GHC will just shrug, but by adding a class constraint to the definition's context, you force the issue. A classic, minimalist example of this problem--class constraints on types that don't appear in the function signature--is the function "show . read". The type is just String -> String, but the behavior depends on an unknown intermediate type.
In my real code I need to define the data instance like:
-- instance (Monad m) => Data (Foo m) a
Which, by itself is fine. But that results in my needing to add (Monad m) to the 'bar' function. And that is what I can't figure out how to do..
The question you should answer first is: How do you expect the bar function to know which monad to use--or, if it doesn't matter which monad it picks, why do you care that it's given a monad at all? - C.
participants (2)
-
C. McCann -
Jeremy Shaw