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.