Issue writing instance for MonadTransControl

[MichaelXavier]

Hi, I've been struggling with this one for the better part of a day. I think this may be an issue that can be easily solved with clever type annotations but for the life of me I can't figure it out. Here's the minimal case reduced from my problem:

newtype FooT m a = FooT { runFooT :: m a -> m a }

instance MonadTrans FooT where
  lift f = FooT $ \_ -> f


instance MonadTransControl FooT where
   type StT FooT a = a
   liftWith f = FooT $ \r -> f $ \t -> runFooT t r
   restoreT = FooT . const
   {-# INLINABLE liftWith #-}
   {-# INLINABLE restoreT #-}

and the error:

Main.hs:18:50:
    Could not deduce (m ~ n)
    from the context (Monad m)
      bound by the type signature for
                 liftWith :: Monad m => (Run FooT -> m a) -> FooT m a
      at Main.hs:18:4-11
    or from (Monad n)
      bound by a type expected by the context:
                 Monad n => FooT n b -> n (StT FooT b)
      at Main.hs:18:30-50
      ‘m’ is a rigid type variable bound by
          the type signature for
            liftWith :: Monad m => (Run FooT -> m a) -> FooT m a
          at Main.hs:18:4
      ‘n’ is a rigid type variable bound by
          a type expected by the context:
            Monad n => FooT n b -> n (StT FooT b)
          at Main.hs:18:30
    Expected type: n b
      Actual type: m a
    Relevant bindings include
      t :: FooT n b (bound at Main.hs:18:35)
      r :: m a (bound at Main.hs:18:25)
      f :: Run FooT -> m a (bound at Main.hs:18:13)
      liftWith :: (Run FooT -> m a) -> FooT m a (bound at Main.hs:18:4)
    In the second argument of ‘runFooT’, namely ‘r’
    In the expression: runFooT t r

Main.hs:18:50:
    Could not deduce (a ~ b)
    from the context (Monad m)
      bound by the type signature for
                 liftWith :: Monad m => (Run FooT -> m a) -> FooT m a
      at Main.hs:18:4-11
    or from (Monad n)
      bound by a type expected by the context:
                 Monad n => FooT n b -> n (StT FooT b)
      at Main.hs:18:30-50
      ‘a’ is a rigid type variable bound by
          the type signature for
            liftWith :: Monad m => (Run FooT -> m a) -> FooT m a
          at Main.hs:18:4
      ‘b’ is a rigid type variable bound by
          a type expected by the context:
            Monad n => FooT n b -> n (StT FooT b)
          at Main.hs:18:30
    Expected type: n b
      Actual type: m a
    Relevant bindings include
      t :: FooT n b (bound at Main.hs:18:35)
      r :: m a (bound at Main.hs:18:25)
      f :: Run FooT -> m a (bound at Main.hs:18:13)
      liftWith :: (Run FooT -> m a) -> FooT m a (bound at Main.hs:18:4)
    In the second argument of ‘runFooT’, namely ‘r’
    In the expression: runFooT t r

It seems like m undergoes a type change somewhere or the type is ambiguous. I've tried many permutations of scoped type variables and annotation and I can't get m and n to unify. Any ideas?

[basvandijk]

Note the type of liftWith:

liftWith :: Monad m => (Run t -> m a) -> t m a

type Run t = forall n b. Monad n => t n b -> n (StT t b)

So the Run function needs to be able to run t n for all n. However in your:

liftWith f = FooT $ \r -> f $ \t -> runFooT t r

your Run function: \t -> runFooT t r has the type: FooT m a -> m (StT (FooT m) a) where m is bound by the type of your liftWith :: forall m a. (Run FooT -> FooT m a) -> FooT m a

This is a known problem of monad-control and also described in #4.

A solution in monad-control would be to parameterise Run with m as in:

type Run t m = forall a. t m a -> m (StT t a)

However this could lead to some "bad" instances. @andersk do you remember why this was important?