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. _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell