data Bar a m = forall t. (MonadTrans t, Monad (t m)) => Bar (t m a -> m a) (t m Int) data Foo = Foo (forall a m. Monad m => Bar a m)
Is it true that I cannot have a function
foo run op = Foo (Bar run op)
I guess the answer is yes and no. Let's consider the type of 'op': exists t. forall m. (MonadTrans t, Monad m, Monad (t m)) => t m Int obviously, we can't write such a type expression in Haskell. There are two work-arounds however. First, we can perform existential instantiation: that is, replace t with some specific type (type constructor, that is). We should also make sure that MonadTrans t and Monad (t m) constraints are satisfied after such a replacement (the typechecker will complain otherwise). So, we come to one known solution:
myFoo :: Int -> Foo myFoo i = Foo (Bar run op) where run :: Monad m => StateT Int m a -> m a run prog = do (a, s) <- runStateT prog i return a op :: Monad m => StateT Int m Int op = get
Here, we replaced t with the specific type constructor StateT. Another way of handling the above type for 't' -- another way of getting rid of the existential quantification -- is to negate the type expression. In other words, make that 'op' an argument of a function, and be sure that 't' doesn't show up in the result. But that's what our 'Bar' already does: *P> :t Bar Bar :: forall m a t. (Monad (t m), MonadTrans t) => (t m a -> m a) -> t m Int -> Bar a m We note that t is not a function of m, so the order of quantification will indeed be "exists t. forall m. ...". That's how we recover the two-step solution, with Foo and Bar.