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)
Right. Simon pointed out that this is a pretty useless function, but not entirely so, since the result of it is not of type 'forall b. b', but rather of 'forall b. C Int b => b'. Thus, if the C class has a function which takes a 'b' as an argument, then this value does have use.
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 = \_ -> ()
This wasn't quite my original example. The type of bind2 needs to be:
bind2 :: ma -> (a -> (MM2 m b)) -> (MM2 m b)
Which does typecheck. However, you cannot seem to write instances of it: instance Monad2 [] a [a] where return2 x = [x] bind2 l f = MM2 (concatMap (unmm2 . f) l) where unmm2 (MM2 mb) = mb yields our friend "cannot unify mb with [b]", both in hugs and ghc.