Lifting `MonadLogic` through transformers.

[jumper149]

I am working on a library that tries to implement instances for a lot of mtl-style type classes: https://hackage.haskell.org/package/deriving-trans

And now I wondered whether I managed to satisfy all the laws of MonadLogic and generally wanted to confirm that this approach works for MonadLogic and LogicT.

I started with this instance:

instance (LogicT.MonadLogic m, MonadTransControlIdentity t) => LogicT.MonadLogic (Elevator t m) where
  msplit tma = (((\(a, b) -> (a, lift b)) <$>) <$>) $
    liftWithIdentity $ \runT -> LogicT.msplit $ runT tma

I am very confident, that this is lawful, since the MonadTransControlIdentity constraint only allows IdentityT and ReaderT (and coercibles of these) as t.

---

Now the experimental part starts. The logict library implements instances for StateT and recently also WriterT (#33).

So I thought it might be possible to use MonadTransControl from the monad-control library to write the generalized instance instead:

instance (LogicT.MonadLogic m, MonadTransControl t) => LogicT.MonadLogic (Elevator t m) where
  msplit tma = liftWith (\runT -> LogicT.msplit $ runT tma) >>= \case
    Nothing -> pure Nothing
    Just (a, as) -> Just . (, restoreT as) <$> restoreT (pure a)

On first look this does seem to be equivalent to the instances from this library, but I wonder if it will also make sense for ExceptT and all the other transformers that satisfy MonadTransControl such as AccumT, MaybeT and so on.

[jumper149]

After playing around with it for a bit I didn't find any problems except for one.

If you have another Alternative instance Monoid e => Alternative (ExceptT e m) for example, then the MonadLogic laws will break. With Elevator this isn't a problem, but ComposeT's behaviour is a bit unexpected, because there you can have mixed up instances.

[Bodigrim]

@jumper149 is there anyting left to discuss here?

[jumper149]

I wasn't able to confirm that MonadTransControl really gives you the instance you desire. There might still be some problems with laziness.

I've not yet dared to merge this into master: https://github.com/jumper149/deriving-trans/commit/e9b7aa9a61b95ca8ebaf81134a86a76b2bc84394

If this is lawful, that would mean that you can also add instances for WriterT, ExceptT and so on to the logict package.