    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Utils.ExtractIO
    -- Copyright : (c) Brian Schroeder
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Helper typeclass for interoperation with APIs which take IO actions in
    -- negative position.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Utils.ExtractIO where

    import Control.Monad.Except      (ExceptT(ExceptT), runExceptT)
    import Control.Monad.IO.Class    (MonadIO)
    import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT)

    import qualified Control.Monad.Writer.Lazy   as LW
    import qualified Control.Monad.Writer.Strict as SW

    -- | Monads which support 'IO' operations and can extract all 'IO' behavior for
    -- interoperation with functions like 'Control.Concurrent.catches', which takes
    -- an 'IO' action in negative position. This function can not be implemented
    -- for transformers like @ReaderT r@ or @StateT s@, whose resultant 'IO'
    -- actions are a function of some environment or state.
    class MonadIO m => ExtractIO m where
        -- | Law: the @m a@ yielded by 'IO' is pure with respect to 'IO'.
        extractIO :: m a -> IO (m a)

    -- | Trivial IO extraction for 'IO'.
    instance ExtractIO IO where
        extractIO :: forall a. IO a -> IO (IO a)
    extractIO = IO a -> IO (IO a)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    -- | IO extraction for 'MaybeT'.
    instance ExtractIO m => ExtractIO (MaybeT m) where
        extractIO :: forall a. MaybeT m a -> IO (MaybeT m a)
    extractIO = (m (Maybe a) -> MaybeT m a) -> IO (m (Maybe a)) -> IO (MaybeT m a)
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap m (Maybe a) -> MaybeT m a
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (IO (m (Maybe a)) -> IO (MaybeT m a))
    -> (MaybeT m a -> IO (m (Maybe a)))
    -> MaybeT m a
    -> IO (MaybeT m a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (Maybe a) -> IO (m (Maybe a))
    forall a. m a -> IO (m a)
    forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
    extractIO (m (Maybe a) -> IO (m (Maybe a)))
    -> (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> IO (m (Maybe a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MaybeT m a -> m (Maybe a)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT

    -- | IO extraction for 'ExceptT'.
    instance ExtractIO m => ExtractIO (ExceptT e m) where
        extractIO :: forall a. ExceptT e m a -> IO (ExceptT e m a)
    extractIO = (m (Either e a) -> ExceptT e m a)
    -> IO (m (Either e a)) -> IO (ExceptT e m a)
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap m (Either e a) -> ExceptT e m a
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (IO (m (Either e a)) -> IO (ExceptT e m a))
    -> (ExceptT e m a -> IO (m (Either e a)))
    -> ExceptT e m a
    -> IO (ExceptT e m a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (Either e a) -> IO (m (Either e a))
    forall a. m a -> IO (m a)
    forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
    extractIO (m (Either e a) -> IO (m (Either e a)))
    -> (ExceptT e m a -> m (Either e a))
    -> ExceptT e m a
    -> IO (m (Either e a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExceptT e m a -> m (Either e a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT

    -- | IO extraction for lazy 'LW.WriterT'.
    instance (Monoid w, ExtractIO m) => ExtractIO (LW.WriterT w m) where
        extractIO :: forall a. WriterT w m a -> IO (WriterT w m a)
    extractIO = (m (a, w) -> WriterT w m a) -> IO (m (a, w)) -> IO (WriterT w m a)
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap m (a, w) -> WriterT w m a
    forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
    LW.WriterT (IO (m (a, w)) -> IO (WriterT w m a))
    -> (WriterT w m a -> IO (m (a, w)))
    -> WriterT w m a
    -> IO (WriterT w m a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (a, w) -> IO (m (a, w))
    forall a. m a -> IO (m a)
    forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
    extractIO (m (a, w) -> IO (m (a, w)))
    -> (WriterT w m a -> m (a, w)) -> WriterT w m a -> IO (m (a, w))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WriterT w m a -> m (a, w)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    LW.runWriterT

    -- | IO extraction for strict 'SW.WriterT'.
    instance (Monoid w, ExtractIO m) => ExtractIO (SW.WriterT w m) where
        extractIO :: forall a. WriterT w m a -> IO (WriterT w m a)
    extractIO = (m (a, w) -> WriterT w m a) -> IO (m (a, w)) -> IO (WriterT w m a)
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap m (a, w) -> WriterT w m a
    forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
    SW.WriterT (IO (m (a, w)) -> IO (WriterT w m a))
    -> (WriterT w m a -> IO (m (a, w)))
    -> WriterT w m a
    -> IO (WriterT w m a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (a, w) -> IO (m (a, w))
    forall a. m a -> IO (m a)
    forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
    extractIO (m (a, w) -> IO (m (a, w)))
    -> (WriterT w m a -> m (a, w)) -> WriterT w m a -> IO (m (a, w))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WriterT w m a -> m (a, w)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    SW.runWriterT