fundeps for extended Monad definition

[oleg@pobox.com]

Hello!

Simon Peyton-Jones wrote:

> class C a b | a -> b where {}

> instance C Int Int where {}

> f1 :: (forall b. (C Int b) => Int -> b)
> f1 x = undefined

Indeed, this gives an error message 
    Cannot unify the type-signature variable `b' with the type `Int'
        Expected type: Int
        Inferred type: b

The reason, which is thoroughly explained in Simon Peyton-Jones'
message, is that the given type signature is wrong: it should read
	f1 :: (exists b. (C Int b) => Int -> b)

Alas, 'exists' is not an allowed type quantifier. Not explicitly that
is. We can get 'exists' if we use the permitted 'forall' in a negative
position (aka in an existential type).

The following code

> class C a b | a -> b where {}

> instance C Int Int where {}

> newtype M a = M (forall b.(C a b) => b)
> f :: Int -> M Int
> f x = M undefined

typechecks in both Haskell compilers.

Hal Daume's original example works as well:

> newtype MM2 m a = MM2 (forall mb.(Monad2 m a mb) => mb)
       

> class Monad2 m a ma | m a -> ma, ma -> m a where
>   return2 :: a -> ma
>   bind2   :: ma -> (a -> (MM2 m a)) -> (MM2 m a)
>   unused :: m a -> ()
>   unused  = \_  -> ()

> instance Monad2 [] a [a] where
>        bind2 = error "urk"

Again, it typechecks both in Hugs and GHC.