Requires MonadPlus (ST a) Instance

Question

I'm reading the paper Typed Logical Variables in Haskell, but I'm failing to understand the details of the ultimate implementation. In particular, the backtracking state transformer introduced in section 4. For some reason, unknown to me, GHC believes I require a MonadPlus instance for (ST a) in the function unify, below:

newtype BackT m a = BT { run :: forall b . (a -> m [b]) -> m [b] }

instance (Monad m) => Monad (BackT m) where
 return a   = BT (\k -> k a)
 BT m >>= f = BT (\k -> m (\a -> run (f a) k))

instance (MonadPlus m) => MonadPlus (BackT m) where 
 mzero             = BT (\s -> mzero)
 f `mplus` g = BT (\s -> (run f) s `mplus` (run g) s)

type LP a = BackT (ST a)
type LR   = STRef

type Var s a = LR s (Maybe a)   
data Atom s = VarA (Var s (Atom s)) | Atom String

class Unify b a | a -> b where
 var   :: a -> Maybe (Var b a)
 unify :: a -> a -> LP s ()

instance Unify s (Atom s) where
 var (VarA a) = Just a
 var _        = Nothing

 unify (Atom a) (Atom b) | a == b = return () -- type checks
 unify _        _                 = mzero     -- requires MonadPlus (ST a) instance

I'm unsure what the problem is, and how to fix it. I was under the impression that I understood the preceding discussion and code until this point, but apparently I was mistaken. If someone could point out what's going awry - do I need a MonadPlus (ST a) instance or not? - it would be very helpful.

[EDIT: Clarification] I should have pointed out that the authors appear to claim that mzero, or some variation on mzero, is the appropriate function. I just don't know what the appropriate function is. What I'm wondering is whether I am supposed to make a MonadPlus (ST a) instance or I'm not using the correct function, and have misread something.

Answer 1

mzero is a member of the typeclass MonadPlus. In particular

mzero :: MonadPlus m => m a

The monad that is used for your function unify is LP, which is actually BackT instantiated with ST. You furthermore define an instance of MonadPlus for BackT, that depends on such an instance for the underlying monad. Since ST has no such instance, GHC mocks you.

This is the important part:

instance (MonadPlus m) => MonadPlus (BackT m) where 
  mzero             = BT (\s -> mzero)
  f `mplus` g = BT (\s -> (run f) s `mplus` (run g) s)

In plain english: This is an instance of MonadPlus for BackT m, provided that m is also an instance of MonadPlus. Since m is instanciated with ST, you need that instance for ST. I wonder how you could define a sensible instance of MonadPlus without delegation. I have an idea:

instance MonadPlus (BackT m) where
  mzero = BT (const $ return [])
  mplus (BT f) (BT g) = BT $ \a -> do
    fs <- f a
    gs <- g a
    return $ fs ++ gs

This instance basically concatenates the two output lists. I hope it suits your needs.

Answer 2

The BackT MonadPlus instance probably should use the MonadPlus instance of [] instead of m, like this:

instance (Monad m) => MonadPlus (BackT m) where 
  mzero       = BT (\_ -> return mzero)
  f `mplus` g = BT (\s -> liftM2 mplus (run f s) (run g s))