The Tactic monad is non-associative

[TOTBWF]

First, a quick example of the problem:

printTac :: String -> Tactic Judgement ()
printTac s = Tactic $ \j -> (T $ reportWarning s) >> return (pure ((), j))

tactic "pair1" [t| forall a b. a -> b -> (a,b) |] $ do
  forall
  intros_
  (split >> printTac "a") >> printTac "b"
  assumption


tactic "pair2" [t| forall a b. a -> b -> (a,b) |] $ do
  forall
  intros_
  split >> (printTac "a" >> printTac "b")
  assumption

Running the 1st tactic will print out "aabb", and running the 2nd will print out "abab".

The core of this issue is that ProofState is not a monad transformer. I'm not sure exactly how to fix this at this point.

[TOTBWF]

After messing around for a while, I think I have come to a solution. The general idea is as follows:

newtype TacticT jdg ext m a = TacticT { unTacticT :: jdg -> Client (a, jdg) ext m ext }

instance (Monad m) => Functor (TacticT jdg ext m) where
  fmap f (TacticT t) = TacticT $ (request . first f) \>\ t

instance (Monad m) => Applicative (TacticT jdg ext m) where
  pure a = TacticT $ \j -> request (a, j)
  (TacticT tf) <*> (TacticT ta) = TacticT $ (\(f, j) -> (request . first (f $)) >\\ ta j) \>\ tf

instance (Monad m) => Monad (TacticT jdg ext m) where
  return = pure
  (TacticT t) >>= k = TacticT $ (\(a, j) -> unTacticT (k a) j) \>\ t

instance MonadTrans (TacticT jdg ext) where
  lift m = TacticT $ \j -> do
    a <- lift m
    request (a, j)

instance (MonadIO m) => MonadIO (TacticT jdg ext m) where
  liftIO m = TacticT $ \j -> do
    a <- liftIO m
    request (a, j)
runTactic :: (Monad m, Show jdg) => TacticT jdg ext m a -> jdg -> m ext
runTactic (TacticT t) j = runEffect $ ((\(_, j) -> fail $ "Unsolved Goal:" ++ show j) >+> t) j

All that needs to be done is to figure out what do do when all of the subgoals are not proved,
and how to dump the intermediate proof state.

EDIT: Slight update: It seems to be very difficult to collect together all of the unsolved goals.
What we are essentially doing here is a streaming, depth-first traversal through all of the subgoals, solving them as we go. Therefore, when we hit our first unsolved goal, we have to bail out.

[TOTBWF]

With a bit of massaging and mmorph magic, I believe I have ironed out all of the problems!

(<..>) :: (Monad m) => TacticT jdg ext m () -> [TacticT jdg ext m ()] -> TacticT jdg ext m ()
(TacticT t) <..> ts = TacticT $ \j -> flip evalStateT (ts ++ repeat (pure ())) $ distribute $ applyTac >\\ (hoist lift $ t j)
  where
    applyTac :: (Monad m) => ((), jdg) -> Client ((), jdg) ext (StateT [TacticT jdg ext m ()] m) ext
    applyTac (_, j) = do
      t <- gets (unTacticT . head)
      modify tail
      hoist lift $ t j

runTacticT :: (Monad m, Extract ext) => TacticT jdg ext m () -> jdg -> m (ext, [jdg])
runTacticT (TacticT t) j = fmap (second reverse) $ flip runStateT [] $ runEffect $ server +>> (hoist lift $ t j)
  where
    server :: (MonadState [jdg] m, Extract ext) => ((), jdg) -> Server ((), jdg) ext m ext
    server (_, j) = do
      modify (j:)
      respond hole >>= server

All that remains is a good Alternative instance, which should be pretty easy.

[TOTBWF]

Turns out the MonadPlus/Alternative instances are a bit trickier than I thought, due to Proxy from pipes lack of MonadPlus/Alternative instances. (see here)

One option would be to use Alt instead, and implement it using catchError. IMO this fits the semantics better.