Generating a Rank2Type within a Monad

Question

So I superfically understand Rank2Types, but when I try the following

{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}

import Data.Machine

f :: IO (Process a a)
f = return . auto $ id

GHC coughs out

Couldn't match type `MachineT m0 (Is a0) a0'
              with `forall (m :: * -> *). Monad m => MachineT m (Is a) a'
Expected type: IO (Process a a)
  Actual type: IO (MachineT m0 (Is a0) a0)
In the expression: return . auto $ id
In an equation for `f': f = return . auto $ id
Failed, modules loaded: none.

So as far as I can see, GHC won't allow me to put a forall in a Monad. Is there a principled, quantification logic reason for this, or is this simply a limitation of GHC? Or am I simply doing something silly?

Answer 1

Your particular example can be made to work as follows:

{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}

import Data.Machine

f = (return :: (forall a. Process a a) -> IO (forall a. Process a a)) (auto id)

As Carl says, you have to annotate functions that you want to use impredicatively, such as return here. Even then, working with impredicative types in GHC is somewhat fragile. I wouldn't recommend it. The reasons for the restrictions are simply that it's tricky to perform type inference in the presence of impredicative types, and additionally, Haskell's surface language has no proper syntax to specify the type at which you want to instantiate a polymorphic function.

A common workaround is to wrap stuff up in a newtype:

data PolyProcess = PP (forall a. Process a a)

f' :: IO PolyProcess
f' = return $ PP $ auto $ id