Why is this not a case of the restricted monad limitation?

Question

In the following code snippet I initially believed to have a restricted monad error (I forgot to add the Monad m => in the instance Monad (Transform m a) definition). Having read quite a bit about restricted monads I wonder why this here happens to be ok:

{-# LANGUAGE GADTs #-}

data Next a where
    Todo :: a -> Next a
    Done :: Next a

instance Functor Next where
    fmap f Done = Done
    fmap f (Todo a) = Todo (f a)

data Transform m a b = Monad m => Transform ( m(Next a) -> m(Next b) )

instance Functor (Transform m a) where
    fmap f (Transform ta) = Transform tb where
        tb ma = ta ma >>= return . (fmap f)

instance Applicative (Transform m a) where
    pure = return
    mf <*> ma = do
        f <- mf
        a <- ma
        return (f a)

instance Monad m => Monad (Transform m a) where
    return b = Transform (t b) where                
        t b _ = return $ Todo b
    (Transform t) >>= f = Transform (\ma -> do     
        a <- ma
        case a of
            Done -> return Done
            --Todo a' -> ...
        )

The example is rather contrived, I stripped away all irrelevant bits. (The actual problem at hand is related to this.) The crucial part is the Monad m restriction in Transform.

I don't quite see how this is different from the often-cited canonical Set-as-a-monad example, which does exhibit the restricted monad limitation.

Answer 1

I don't quite see how this is different from the often-cited canonical Set-as-a-monad example, which does exhibit the restricted monad limitation.

It's different because the constraint isn't on the last type parameter, which is the one which varies in Monad. In the case of Set it is.

Answer 2

Transform is not a restricted monad.

Look at Set. Set is monadic in its one argument, except said argument needs to be Ord. That is, Set is a monad on the subcategory of Hask where all the objects are in Ord.

But Transform is not a monad in the first place. Transform :: (* -> *) -> * -> * -> *, but Monad applies to things of kind * -> * (if you're going to go full category theorist, monads in general are endofunctors and should roughly have kind k -> k for some k, but Transform doesn't really fit that wider template either). The thing that is a monad is Transform m a when m is a monad. Transform m a is monad on all of Hask, as long as m is also a monad. You see the difference? Transform m a given Monad m operates on every type there is. But there is nothing I can put in the blank to make "Set given ___ operates on every type there is", because the restriction is going on the parameter that Set is monadic in, while Transform m a does not have a restriction on the type it is monadic in, but on one of the types that makes it up.