[Haskell-cafe] ambiguous type variable problem when using forall, multiparameter type classes, and constraints on polymorphic values (and syb-with-class)

[Jeremy Shaw]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100521/cbd2e965/attachment.html