[Haskell-cafe] Generalizing "unlift" functions with monad-control

30 Mar 2015

      I'm trying to extract an "unlift" function from monad-control, which would
allow stripping off a layer of a transformer stack in some cases. It's easy
to see that this works well for ReaderT, e.g.:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
import Control.Monad.Trans.Control
import Control.Monad.Trans.Reader

newtype Unlift t = Unlift { unlift :: forall n b. Monad n => t n b -> n b }

askRun :: Monad m => ReaderT r m (Unlift (ReaderT r))
askRun = liftWith (return . Unlift)

The reason this works is that the `StT` associated type for `ReaderT` just
returns the original type, i.e. `type instance StT (ReaderT r) m a = a`. In
theory, we should be able to generalize `askRun` to any transformer for
which that applies. However, I can't figure out any way to express that
generalized type signature in a way that GHC accepts it. It seems like the
following should do the trick:

askRunG :: ( MonadTransControl t
           , Monad m
           , b ~ StT t b
           )
        => t m (Unlift t)
askRunG = liftWith (return . Unlift)

However, I get the following error message when trying this:

foo.hs:11:12:
    Occurs check: cannot construct the infinite type: b0 ~ StT t b0
    The type variable ‘b0’ is ambiguous
    In the ambiguity check for the type signature for ‘askRunG’:
      askRunG :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) b.
                 (MonadTransControl t, Monad m, b ~ StT t b) =>
                 t m (Unlift t)
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘askRunG’:
      askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =>
                 t m (Unlift t)

Adding AllowAmbiguousTypes to the mix provides:

foo.hs:17:30:
    Could not deduce (b1 ~ StT t b1)
    from the context (MonadTransControl t, Monad m, b ~ StT t b)
      bound by the type signature for
                 askRunG :: (MonadTransControl t, Monad m, b ~ StT t b) =>
                            t m (Unlift t)
      at foo.hs:(12,12)-(16,25)
      ‘b1’ is a rigid type variable bound by
           the type forall (n1 :: * -> *) b2.
                    Monad n1 =>
                    t n1 b2 -> n1 (StT t b2)
           at foo.hs:1:1
    Expected type: Run t -> Unlift t
      Actual type: (forall (n :: * -> *) b. Monad n => t n b -> n b)
                   -> Unlift t
    Relevant bindings include
      askRunG :: t m (Unlift t) (bound at foo.hs:17:1)
    In the second argument of ‘(.)’, namely ‘Unlift’
    In the first argument of ‘liftWith’, namely ‘(return . Unlift)’

I've tested with both GHC 7.8.4 and 7.10.1. Any suggestions?

[Haskell-cafe] Generalizing "unlift" functions with monad-control

Michael Snoyman