Using Logic monad to backtrack upon exception thrown with ExceptT

Question

I'd like to use the Logic monad to ensure that error-throwing code (in a monad stack including ExcepT) backtracks upon throwing an error. Here's a simple example:

newtype FooT m a = FooT { unFooT :: ExceptT String m a }
  deriving (Functor, Applicative, Monad, MonadTrans, MonadError String, MonadFail)
 

foo :: FooT Logic String
foo = do
  let validate s = if s == "cf" then return s else throwError "err"
  let go = do
        first <- msum (map return ['a', 'b', 'c'])     
        second <- msum (map return ['d', 'e', 'f'])
        traceM $ "Guess: " ++ [first, second]
        validate [first, second]
  go `catchError` const mzero

testfoo :: IO ()
testfoo = do
  let r = observe $ runExceptT $ unFooT foo
  case r of
    Left e -> print $ "Error: " ++ e
    Right s -> print $ "Result: " ++ 

This doesn't backtrack; it produces no results. I can make it backtrack by lifting the choice operations (ie, use lift (msum ...) instead of the plain msum call there is now). However, for a variety of reasons I'd like to be able to write code in the ExceptT monad and basically just lift the MonadPlus instance from the Logic monad into the transformed version. I tried to write a custom MonadPlus instance to accomplish this here:

instance MonadPlus m => MonadPlus (FooT m) where
  mzero = lift mzero
  mplus (FooT a) (FooT b) = lift $ do
    ea <- runExceptT a
    case ea of
      Left _ -> do
        eb <- runExceptT b
        case eb of
          Left _ -> mzero
          Right y -> return y
      Right x -> do
        eb <- runExceptT b
        case eb of
          Left _ -> return x
          Right y -> return x `mplus` return y

The same code works for the Alternative instance as well. However, this doesn't actually help; it still doesn't backtrack. Is there something wrong with this instance? Is there a better way to solve this problem? Am I trying to do something that doesn't make sense? At the end of the day I can always just lift everything, but would prefer to avoid doing so.

Edit: Have been messing around some more. My MonadPlus instance above works if I use mplus but does not work if I use msum like I did above...

Answer 1

Use this instance of MonadPlus/Alternative:

instance (Alternative m, Monad m) => Alternative (FooT m) where
  empty = FooT (ExceptT empty)
  FooT (ExceptT a) <|> FooT (ExceptT b) = FooT (ExceptT (a <|> b))

Note: Alternative and MonadPlus are redundant, so it's simpler to just implement Alternative, and use Data.Foldable.asum instead of msum.

The one you implemented is not too different from the one that's already on ExceptT, and does not really use the Alternative m instance. Make sure to use (<|>) specialized to m to benefit from backtracking.