rank 2-polymorphism and type checking

[Ashley Yakeley]

At 2001-10-24 01:08, Simon Peyton-Jones wrote:

>So I'm interested to know: if GHC allowed arbitrarily-ranked types, who
>would use them?

I would. Right now I have a class for 'IO lifted monads', that is, monads 
from which one can call IO actions:

    class (Monad m) => IOLiftedMonad m where
        {
        callIOWithMap	:: ((m a -> IO a) -> IO b) -> m b;
        callIO		     	:: IO a -> m a;
        callIO        = callIOWithMap . const;
        };

The 'callIOWithMap' function allows such things as 'catch' to be defined 
over the monad:

    class (IOLiftedMonad m) => IsJVMMonad m where
        ...

    jvmCatch :: (IsJVMMonad m) => m a -> (JThrowable -> m a) -> m a;
    jvmCatch foo catchClause = callIOWithMap (\map -> catch (map foo) (\x 
-> map (do
        {
        exRef <- callIOWithEnv vmGetClearException;
        noEx <- callIO (getIsNothing exRef);
        if noEx
            then (callIO (ioError x))
            else catchClause (MkJVMRef exRef);
        })));

Now this is fine, because both occurences of 'map' have the same type. 
But I recently discovered this doesn't work if the map is used with 
different types. For instance, GHC 5.02 won't compile this:

    test :: (IOLiftedMonad m) => m a -> m b -> m (a,b);
    test ma mb = callIOWithMap (\map -> do
        {
        a <- map ma;
        b <- map mb;
        return (a,b);
        });

It looks like what I really need is this:

    callIOWithMap	:: ((forall a. (m a -> IO a)) -> IO b) -> m b;

Is that correct? But GHC doesn't allow it...

-- 
Ashley Yakeley, Seattle WA