fundeps for extended Monad definition

[Hal Daume III]

Hi all,

I'm hoping someone can explain some weirdnesses to me.  I want to have a
class that's like the standard Monad class, but is a bit more
general.  That is, I want:

class Monad2 m a ma | m a -> ma, ma -> m a where
  return2 :: a -> ma
  bind2   :: Monad2 m b mb => ma -> (a -> mb) -> mb
  _unused :: m a -> ()
  _unused  = \_  -> ()

Here, all the real work happens in the combined "mb" parameter.  The
_unused definition is just to get Hugs to realize that 'm' should be of
kind * -> * (for GHC, a kind definition does the same thing).

I want to be able to define instances like:

instance Monad2 [] a [a] where
  return2 x = [x]
  bind2 l f = concatMap f l

However, in GHC, if I just give the instance declaration (without the
function definitions), we get:

    Cannot unify the type-signature variable `mb' with the type `[b]'
	Expected type: [b]
	Inferred type: mb
    When using functional dependencies to combine
      Monad2 [] a [a],
	arising from the instance declaration at
/nfs/isd/hdaume/projects/Trials/UsefulDTs/UsefulDTs.hs:114
      Monad2 [] b mb,
	arising from a type signature at
/nfs/isd/hdaume/projects/Trials/UsefulDTs/UsefulDTs.hs:114
    When trying to generalise the type inferred for `bind2'
	Signature type:     forall a mb1 b1.
			    (Monad2 [] b1 mb1) =>
			    [a] -> (a -> mb1) -> mb1
	Type to generalise: forall mb1 b1.
			    (Monad2 [] b1 mb1) =>
			    [a] -> (a -> mb1) -> mb1

This doesn't make sense to me.  Hugs accepts this without
complaint.  Here's why I don't understand it:

We know that m is [].  We have an instance definition (the one we're
defining) that says that for any type x, we have 'Monad2 [] x [x]' where
[] and x determine [x].  This should tell us that mb=[b], but somehow GHC
doesn't get that (or there's something wrong with my reasoning).

When the funciton definitions are provided for the instance, GHC
complains:

/nfs/isd/hdaume/projects/Trials/UsefulDTs/UsefulDTs.hs:119:
    Cannot unify the type-signature variable `mb' with the type `[b]'
	Expected type: a -> [b]
	Inferred type: a -> mb
    In the first argument of `concatMap', namely `f'
    In the definition of `bind2': concatMap f l

and Hugs complains similarly:

*** Expected type : (Monad2 [] a [a], Monad2 [] b c) => [a] -> (a -> c) ->
c
*** Inferred type : (Monad2 [] a [a], Monad2 [] b [c]) => [a] -> (a ->
[c]) -> [c]


Both are saying that they don't know that mb=[b], but I think the fundeps
guarentee this.

Note that if we change the type definition of bind2 to:

  bind2 :: Monad2 m b mb => ma -> (a -> m b) -> m b

then Hugs accepts the instance declaration but GHC complains as it did the
first time.

Can someone explain which is right and why?

Thanks!

 - Hal

--
Hal Daume III

 "Computer science is no more about computers    | hdaume@isi.edu
  than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume