`liftWith` for `MockT`

[ChickenProp]

I've been porting a codebase from monad-mock where we've been using the MonadTransControl instance. That's not available for HMock. Currently I've got an orphan instance of it that's definitely not safe in general, but that works in the places where I use it. But I think it might be possible to provide a function that's basically liftWith specialized to MockT, that could be used safely.

To illustrate, here's the function in question, and the code I'm testing it with:

import qualified Test.HMock.Internal.State as HMockI
-- And a bunch of other imports

-- | Basically `liftWith`
liftMockWith
  :: forall m a
   . ((forall n b . Coercible m n => MockT n b -> n b) -> m a)
  -> MockT m a
liftMockWith run = HMockI.MockT $ ReaderT $ \state ->
  let runArg :: forall n b . MockT n b -> n b
      runArg =
        let changeState :: HMockI.MockState m -> HMockI.MockState n
            changeState (HMockI.MockState {..}) = HMockI.MockState
              { mockExpectSet       = unsafeCoerce mockExpectSet
              , mockDefaults        = unsafeCoerce mockDefaults
              , mockAllowUnexpected = unsafeCoerce mockAllowUnexpected
              , mockSideEffects     = unsafeCoerce mockSideEffects
              , mockParent          = unsafeCoerce mockParent
              , ..
              }
        in  flip runReaderT (changeState state) . HMockI.unMockT
  in  run runArg

-- Test it:
class Monad m => MonadFilesystem m where
  readF :: FilePath -> m String
  writeF :: FilePath -> String -> m ()

copyFile :: MonadFilesystem m => FilePath -> FilePath -> m ()
copyFile a b = readF a >>= writeF b

makeMockable [t|MonadFilesystem|]

spec :: Spec
spec =
  it "Test mock" $ do
    return () :: IO ()
    runIdentityT $ do
      return () :: IdentityT IO ()
      HMock.runMockT $ do
        return () :: HMock.MockT (IdentityT IO) ()
        expect $ ReadF "foo.txt" |-> "contents"
        expect $ WriteF "bar.txt" "contents" |-> ()
        liftMockWith $ \run -> do
          return () :: IdentityT IO ()
          liftIO $ run $ do
            copyFile "foo.txt" "bar.txt" :: MockT IO ()

I've included some type annotations partly as a hint to the typechecker and partly to make it a bit clearer what's going on.

This works fine, despite the unsafeCoerce. We can also move one or both expect calls to directly above copyFile, inside the run block.

We can use the same basic function to implement an orphan instance of MonadTransControl. (With StT MockT a = a and restoreT = lift.) And then if we replace liftMockWith in that code with liftWith, there's still no problem. (At least not at -O0. There's a lot of edge cases I haven't tested thoroughly yet.)

But it doesn't work if we replace IdentityT with a version of itself that's been implemented with data instead of newtype. That is, instead of importing IdentityT, define

data IdentityT m a = IdentityT { runIdentityT :: m a }
  deriving stock Functor

instance Applicative m => Applicative (IdentityT m) where
  pure = IdentityT . pure
  IdentityT f <*> IdentityT x = IdentityT $ f <*> x

instance Monad m => Monad (IdentityT m) where
  IdentityT x >>= f = IdentityT $ x >>= runIdentityT . f

instance MonadIO m => MonadIO (IdentityT m) where
  liftIO = IdentityT . liftIO

and suddenly we get a segfault.

       uncaught exception: ErrorCall
       Wrong arguments: writeF "bar.txt" "\1099511628032zsh: segmentation fault (core dumped)  cabal run $GHC_LINK_OPTS -O0 testnofork -- -m "Test mock"

Presumably we've gone from doing unsafeCoerce between things that are coercible, to between things that aren't. And if we go back to liftMockWith, using our data-based IdentityT, we get a comile error:

    • Couldn't match representation of type ‘IdentityT IO’
                               with that of ‘IO’
        arising from a use of ‘run’
      The data constructor ‘ghc-prim-0.6.1:GHC.Types.IO’
        of newtype ‘IO’ is not in scope

(For either version of IdentityT, and either liftWith or liftMockWith, we can remove the liftIO and it works. Then the type of the copyFile line is MockT (IdentityT IO) (), and we're coercing between a thing and itself.)

So a big question here is, is that unsafeCoerce actually safe? Ultimately the things we're coercing are all either TVar [Step {m/n}] or TVar (ExpectSet (Step {m/n})). Step has type role nominal, so coerce isn't allowed unless m ~ n, but that doesn't prove it's unsafe. I think the thing I'd be most worried about is it has a Typeable m constraint. But I don't currently know where that comes from or if it's a problem here.

If the unsafeCoerce actually is unsafe, then another option might be to restrict the type further, to m ~ n - at that point it looks similar to withMockT, I'm not sure what the relationship is between them but maybe withMockT already gives us everything we're going to get here.

liftMockWith ::              ((forall a . MockT m a -> m a) -> m b)
withMockT    :: MonadIO m => ((forall a . MockT m a -> m a) -> MockT m b) -> m b

(It's also possible withMockT will be sufficient for what I want to do. I don't currently think so, but I haven't fully explored the possibility. edit: looked into it now, I'm pretty sure it won't.)

---

Sorry this is kind of rambling. I guess the main questions I'm wondering here are

1. Does the liftMockWith implementation above seem safe?
2. Would you consider adding it?

[ChickenProp]

Another possibility if unsafeCoerce isn't safe, is that there might be some way to turn a Step m into a Step n without coercing, even if the Coercible constraint is required. If so, it would presumably be possible to do read from the TVars in the state, convert the Steps, put them into new TVars which go into a new state, run something with that state, and then do the reverse to update the original state. Presumably you lose thread safety at that point though.

[ChickenProp]

I think the thing I'd be most worried about is it has a Typeable m constraint. But I don't currently know where that comes from or if it's a problem here.

So I looked into it and it seems this can be removed. The place it's needed is a few uses of cast in MockMethod. But all of those uses are casting between things with the same m. That is, we can replace these uses with calls to

castStep
  :: forall cls1 cls2 name1 name2 m r1 r2
   . ( KnownSymbol name1, KnownSymbol name2
     , Typeable cls1, Typeable cls2
     , Typeable r1, Typeable r2
     , Typeable m
     )
  => Located (SingleRule cls1 name1 m r1)
  -> Maybe (Located (SingleRule cls2 name2 m r2))
castStep = cast

and the types line up. cast here imposes Typeable m, but if we implement this differently we don't need it:

castStep
  :: forall cls1 cls2 name1 name2 m r1 r2
   . ( KnownSymbol name1, KnownSymbol name2
     , Typeable cls1, Typeable cls2
     , Typeable r1, Typeable r2
     )
  => Located (SingleRule cls1 name1 m r1)
  -> Maybe (Located (SingleRule cls2 name2 m r2))
castStep (Loc l rule) = do
  Refl :: r1 :~: r2 <- eqT
  Refl :: name1 :~: name2 <- eqT
  Refl :: cls1 :~: cls2 <- eqT
  Just (Loc l rule)

With this change we can remove m from MockableMethod, making it just

type MockableMethod
  (cls :: (Type -> Type) -> Constraint)
  (name :: Symbol)
  (r :: Type) =
  (Mockable cls, KnownSymbol name, Typeable r)

and (when we fix up the references to MockableMethod) this compiles and passes tests.

We still have type role nominal for m in Step m, so we still need unsafeCoerce. But is it safe? I think it should be. Step m ultimately contains some number of Matcher cls name m r and some number of Action cls name m r, and no constraints on m. Matcher and Action are both data families of the MockableBase class, parameterized on their first argument. According to this SO answer, data families have nominal type roles for all their arguments, but that's only necessary for the parameterized ones, and representational would be fine for the others. (I haven't read through the thread that answer links to, maybe there's nuance I'm not getting.)

...unfortunately the test still crashes with liftWith and a data-based IdentityT, so apparently not. I don't know what's up with that.

(But removing the Typeable m constraint is still kinda helpful for me, since I've had to add a few while porting from monad-mock.)

[cdsmith]

I've been reading this, intending to get to it when I have time to think it through. I suspect that unsafeCoerce cannot be made safe here. MockState contains actual actions that run in the MockT m monad and they cannot just be coerced to a different monad with a different runtime representation.

I will look at your technique for removing the Typeable constraint on the monad though. That seems useful.

[cdsmith]

I'm not really familiar with MonadTransControl, but it's likely I can provide an instance. MockT is just ReaderT, after all.

[ChickenProp]

I suspect that unsafeCoerce cannot be made safe here. MockState contains actual actions that run in the MockT m monad and they cannot just be coerced to a different monad with a different runtime representation.

Ah, to clarify, do you think unsafeCoerce is unsafe in practice even if the monads are coercible?

I'm not really familiar with MonadTransControl, but it's likely I can provide an instance. MockT is just ReaderT, after all.

So the problem is that it's ReaderT where the thing being read is parameterized over the monad. Inside a ReaderT Foo IO a we can get a Foo and pass it into a ReaderT Foo (IdentityT IO) b. But here, inside a ReaderT (MonadState IO) IO a, we'd need to get a MonadState (IdentityT IO) and pass it into a ReaderT (MonadState (IdentityT IO)) (IdentityT IO) b.

I'd love to be wrong, though.

[ChickenProp]

...unfortunately the test still crashes with liftWith and a data-based IdentityT, so apparently not. I don't know what's up with that.

Oh, having slept on it, I was confused. The argument above was that removing the Typeable constraint would allow Step m to have a representational type role for m. That would give us Coercible m n => Coercible (Step m) (Step n). So it suggests unsafeCoerce should be fine between coercible monads, even though GHC currently assigns a nominal role there. So it suggests liftMockWith would be safe.

But it doesn't give us Coercible (Step m) (Step n) in general, that would need a phantom role, so we still wouldn't expect liftWith between monads with different representations to be safe.

[ChickenProp]

MockState contains actual actions that run in the MockT m monad

So I think I hadn't fully appreciated this. This is from |=>, right? Which, yeah, lets us run arbitrary monadic actions in response to a mocked action. Which means even if the two monads are coercible, we're likely violating some kind of expectation. In my case, the monads I'm using are tagged with a database transaction isolation level, and this means I could run a database query in a different level than I think I'm in.

I don't think this is a problem in practice for me, but it's definitely a problem in theory. HMock's design might just not work with this kind of thing.