    -------------------------------------------------------------------------
    -- |
    -- Module      : Control.Monad.Logic
    -- Copyright   : (c) 2007-2014 Dan Doel,
    --               (c) 2011-2013 Edward Kmett,
    --               (c) 2014      Roman Cheplyaka,
    --               (c) 2020-2021 Andrew Lelechenko,
    --               (c) 2020-2021 Kevin Quick
    -- License     : BSD3
    -- Maintainer  : Andrew Lelechenko <andrew.lelechenko@gmail.com>
    --
    -- Adapted from the paper
    -- <http://okmij.org/ftp/papers/LogicT.pdf Backtracking, Interleaving, and Terminating Monad Transformers>
    -- by Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry.
    -- Note that the paper uses 'MonadPlus' vocabulary
    -- ('mzero' and 'mplus'),
    -- while examples below prefer 'empty' and '<|>'
    -- from 'Alternative'.
    -------------------------------------------------------------------------

    {-# LANGUAGE CPP                   #-}
    {-# LANGUAGE DeriveFoldable        #-}
    {-# LANGUAGE DeriveFunctor         #-}
    {-# LANGUAGE DeriveTraversable     #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE RankNTypes            #-}
    {-# LANGUAGE UndecidableInstances  #-}

    #if __GLASGOW_HASKELL__ >= 704
    {-# LANGUAGE Safe #-}
    #endif

    module Control.Monad.Logic (
        module Control.Monad.Logic.Class,
        -- * The Logic monad
        Logic,
        logic,
        runLogic,
        observe,
        observeMany,
        observeAll,
        -- * The LogicT monad transformer
        LogicT(..),
        runLogicT,
        observeT,
        observeManyT,
        observeAllT,
        fromLogicT,
        fromLogicTWith,
        hoistLogicT,
        embedLogicT
      ) where

    import Control.Applicative

    import Control.Monad
    import qualified Control.Monad.Fail as Fail
    import Control.Monad.Identity (Identity(..))
    import Control.Monad.IO.Class (MonadIO(..))
    import Control.Monad.Trans (MonadTrans(..))
    #if MIN_VERSION_base(4,8,0)
    import Control.Monad.Zip (MonadZip (..))
    #endif

    import Control.Monad.Reader.Class (MonadReader(..))
    import Control.Monad.State.Class (MonadState(..))
    import Control.Monad.Error.Class (MonadError(..))

    #if !MIN_VERSION_base(4,8,0)
    import Data.Monoid (Monoid (..))
    #endif

    #if MIN_VERSION_base(4,9,0)
    import Data.Semigroup (Semigroup (..))
    #endif

    import qualified Data.Foldable as F
    import qualified Data.Traversable as T

    import Control.Monad.Logic.Class

    -------------------------------------------------------------------------
    -- | A monad transformer for performing backtracking computations
    -- layered over another monad @m@.
    --
    -- When @m@ is 'Identity', 'LogicT' @m@ becomes isomorphic to a list
    -- (see 'Logic'). Thus 'LogicT' @m@ for non-trivial @m@ can be imagined
    -- as a list, pattern matching on which causes monadic effects.
    --
    newtype LogicT m a =
        LogicT { forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r }

    -------------------------------------------------------------------------
    -- | Extracts the first result from a 'LogicT' computation,
    -- failing if there are no results at all.
    #if !MIN_VERSION_base(4,13,0)
    observeT :: Monad m => LogicT m a -> m a
    #else
    observeT :: MonadFail m => LogicT m a -> m a
    #endif
    observeT :: forall (m :: * -> *) a. MonadFail m => LogicT m a -> m a
    observeT LogicT m a
    lt = LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    lt (m a -> m a -> m a
    forall a b. a -> b -> a
    const (m a -> m a -> m a) -> (a -> m a) -> a -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return) (String -> m a
    forall a. String -> m a
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail String
    "No answer.")

    -------------------------------------------------------------------------
    -- | Extracts all results from a 'LogicT' computation, unless blocked by the
    -- underlying monad.
    --
    -- For example, given
    --
    -- >>> let nats = pure 0 <|> fmap (+ 1) nats
    --
    -- some monads (like 'Identity', 'Control.Monad.Reader.Reader',
    -- 'Control.Monad.Writer.Writer', and 'Control.Monad.State.State')
    -- will be productive:
    --
    -- >>> take 5 $ runIdentity (observeAllT nats)
    -- [0,1,2,3,4]
    --
    -- but others (like 'Control.Monad.Except.ExceptT',
    -- and 'Control.Monad.Cont.ContT') will not:
    --
    -- >>> take 20 <$> runExcept (observeAllT nats)
    --
    -- In general, if the underlying monad manages control flow then
    -- 'observeAllT' may be unproductive under infinite branching,
    -- and 'observeManyT' should be used instead.
    observeAllT :: Applicative m => LogicT m a -> m [a]
    observeAllT :: forall (m :: * -> *) a. Applicative m => LogicT m a -> m [a]
    observeAllT LogicT m a
    m = LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    m (([a] -> [a]) -> m [a] -> m [a]
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (([a] -> [a]) -> m [a] -> m [a])
    -> (a -> [a] -> [a]) -> a -> m [a] -> m [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (:)) ([a] -> m [a]
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [])

    -------------------------------------------------------------------------
    -- | Extracts up to a given number of results from a 'LogicT' computation.
    observeManyT :: Monad m => Int -> LogicT m a -> m [a]
    observeManyT :: forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
    observeManyT Int
    n LogicT m a
    m
        | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 = [a] -> m [a]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        | Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    m (\a
    a m [a]
    _ -> [a] -> m [a]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [a
    a]) ([a] -> m [a]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [])
        | Bool
    otherwise = LogicT m (Maybe (a, LogicT m a))
    -> forall r. (Maybe (a, LogicT m a) -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT (LogicT m a -> LogicT m (Maybe (a, LogicT m a))
    forall a. LogicT m a -> LogicT m (Maybe (a, LogicT m a))
    forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
    msplit LogicT m a
    m) Maybe (a, LogicT m a) -> m [a] -> m [a]
    forall {m :: * -> *} {a} {p}.
    Monad m =>
    Maybe (a, LogicT m a) -> p -> m [a]
    sk ([a] -> m [a]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [])
     where
     sk :: Maybe (a, LogicT m a) -> p -> m [a]
    sk Maybe (a, LogicT m a)
    Nothing p
    _ = [a] -> m [a]
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
     sk (Just (a
    a, LogicT m a
    m')) p
    _ = (a
    aa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :) ([a] -> [a]) -> m [a] -> m [a]
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    `liftM` Int -> LogicT m a -> m [a]
    forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
    observeManyT (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) LogicT m a
    m'

    -------------------------------------------------------------------------
    -- | Runs a 'LogicT' computation with the specified initial success and
    -- failure continuations.
    --
    -- The second argument ("success continuation") takes one result of
    -- the 'LogicT' computation and the monad to run for any subsequent
    -- matches.
    --
    -- The third argument ("failure continuation") is called when the
    -- 'LogicT' cannot produce any more results.
    --
    -- For example:
    --
    -- >>> yieldWords = foldr ((<|>) . pure) empty
    -- >>> showEach wrd nxt = putStrLn wrd >> nxt
    -- >>> runLogicT (yieldWords ["foo", "bar"]) showEach (putStrLn "none!")
    -- foo
    -- bar
    -- none!
    -- >>> runLogicT (yieldWords []) showEach (putStrLn "none!")
    -- none!
    -- >>> showFirst wrd _ = putStrLn wrd
    -- >>> runLogicT (yieldWords ["foo", "bar"]) showFirst (putStrLn "none!")
    -- foo
    --
    runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r
    runLogicT :: forall (m :: * -> *) a r.
    LogicT m a -> (a -> m r -> m r) -> m r -> m r
    runLogicT (LogicT forall r. (a -> m r -> m r) -> m r -> m r
    r) = (a -> m r -> m r) -> m r -> m r
    forall r. (a -> m r -> m r) -> m r -> m r
    r

    -- | Convert from 'LogicT' to an arbitrary logic-like monad transformer,
    -- such as <https://hackage.haskell.org/package/list-t list-t>
    -- or <https://hackage.haskell.org/package/logict-sequence logict-sequence>
    --
    -- For example, to show a representation of the structure of a `LogicT`
    -- computation, @l@, over a data-like `Monad` (such as @[]@,
    -- @Data.Sequence.Seq@, etc.), you could write
    --
    -- @
    -- import ListT (ListT)
    --
    -- 'show' $ fromLogicT @ListT l
    -- @
    #if MIN_VERSION_base(4,8,0)
    fromLogicT :: (Alternative (t m), MonadTrans t, Monad m, Monad (t m))
      => LogicT m a -> t m a
    #else
    fromLogicT :: (Alternative (t m), MonadTrans t, Applicative m, Monad m, Monad (t m))
      => LogicT m a -> t m a
    #endif
    fromLogicT :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (Alternative (t m), MonadTrans t, Monad m, Monad (t m)) =>
    LogicT m a -> t m a
    fromLogicT = (forall x. m x -> t m x) -> LogicT m a -> t m a
    forall (m :: * -> *) (n :: * -> *) a.
    (Applicative m, Monad n, Alternative n) =>
    (forall x. m x -> n x) -> LogicT m a -> n a
    fromLogicTWith m x -> t m x
    forall x. m x -> t m x
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift

    -- | Convert from @'LogicT' m@ to an arbitrary logic-like monad,
    -- such as @[]@.
    --
    -- Examples:
    --
    -- @
    -- 'fromLogicT' = fromLogicTWith d
    -- 'hoistLogicT' f = fromLogicTWith ('lift' . f)
    -- 'embedLogicT' f = 'fromLogicTWith' f
    -- @
    --
    -- The first argument should be a
    -- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
    -- to produce sensible results.
    fromLogicTWith :: (Applicative m, Monad n, Alternative n)
      => (forall x. m x -> n x) -> LogicT m a -> n a
    fromLogicTWith :: forall (m :: * -> *) (n :: * -> *) a.
    (Applicative m, Monad n, Alternative n) =>
    (forall x. m x -> n x) -> LogicT m a -> n a
    fromLogicTWith forall x. m x -> n x
    p (LogicT forall r. (a -> m r -> m r) -> m r -> m r
    f) = n (n a) -> n a
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (n (n a) -> n a) -> (m (n a) -> n (n a)) -> m (n a) -> n a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (n a) -> n (n a)
    forall x. m x -> n x
    p (m (n a) -> n a) -> m (n a) -> n a
    forall a b. (a -> b) -> a -> b
    $
      (a -> m (n a) -> m (n a)) -> m (n a) -> m (n a)
    forall r. (a -> m r -> m r) -> m r -> m r
    f (\a
    a m (n a)
    v -> n a -> m (n a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a -> n a
    forall a. a -> n a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    a n a -> n a -> n a
    forall a. n a -> n a -> n a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> n (n a) -> n a
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (m (n a) -> n (n a)
    forall x. m x -> n x
    p m (n a)
    v))) (n a -> m (n a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure n a
    forall a. n a
    forall (f :: * -> *) a. Alternative f => f a
    empty)

    -- | Convert a 'LogicT' computation from one underlying monad to another.
    -- For example,
    --
    -- @
    -- hoistLogicT lift :: LogicT m a -> LogicT (StateT m) a
    -- @
    --
    -- The first argument should be a
    -- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
    -- to produce sensible results.
    hoistLogicT :: (Applicative m, Monad n) => (forall x. m x -> n x) -> LogicT m a -> LogicT n a
    hoistLogicT :: forall (m :: * -> *) (n :: * -> *) a.
    (Applicative m, Monad n) =>
    (forall x. m x -> n x) -> LogicT m a -> LogicT n a
    hoistLogicT forall x. m x -> n x
    f = (forall x. m x -> LogicT n x) -> LogicT m a -> LogicT n a
    forall (m :: * -> *) (n :: * -> *) a.
    (Applicative m, Monad n, Alternative n) =>
    (forall x. m x -> n x) -> LogicT m a -> n a
    fromLogicTWith (n x -> LogicT n x
    forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n x -> LogicT n x) -> (m x -> n x) -> m x -> LogicT n x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m x -> n x
    forall x. m x -> n x
    f)

    -- | Convert a 'LogicT' computation from one underlying monad to another.
    --
    -- The first argument should be a
    -- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
    -- to produce sensible results.
    embedLogicT :: Applicative m => (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
    embedLogicT :: forall (m :: * -> *) (n :: * -> *) b.
    Applicative m =>
    (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
    embedLogicT forall a. m a -> LogicT n a
    f = (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
    forall (m :: * -> *) (n :: * -> *) a.
    (Applicative m, Monad n, Alternative n) =>
    (forall x. m x -> n x) -> LogicT m a -> n a
    fromLogicTWith m x -> LogicT n x
    forall a. m a -> LogicT n a
    f

    -------------------------------------------------------------------------
    -- | The basic 'Logic' monad, for performing backtracking computations
    -- returning values (e.g. 'Logic' @a@ will return values of type @a@).
    --
    -- __Technical perspective.__
    -- 'Logic' is a
    -- <http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html Boehm-Berarducci encoding>
    -- of lists. Speaking plainly, its type is identical (up to 'Identity' wrappers)
    -- to 'foldr' applied to a given list. And this list itself can be reconstructed
    -- by supplying @(:)@ and @[]@.
    --
    -- > import Data.Functor.Identity
    -- >
    -- > fromList :: [a] -> Logic a
    -- > fromList xs = LogicT $ \cons nil -> foldr cons nil xs
    -- >
    -- > toList :: Logic a -> [a]
    -- > toList (LogicT fld) = runIdentity $ fld (\x (Identity xs) -> Identity (x : xs)) (Identity [])
    --
    type Logic = LogicT Identity

    -------------------------------------------------------------------------
    -- | A smart constructor for 'Logic' computations.
    logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a
    logic :: forall a. (forall r. (a -> r -> r) -> r -> r) -> Logic a
    logic forall r. (a -> r -> r) -> r -> r
    f = (forall r.
     (a -> Identity r -> Identity r) -> Identity r -> Identity r)
    -> LogicT Identity a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r.
      (a -> Identity r -> Identity r) -> Identity r -> Identity r)
     -> LogicT Identity a)
    -> (forall r.
        (a -> Identity r -> Identity r) -> Identity r -> Identity r)
    -> LogicT Identity a
    forall a b. (a -> b) -> a -> b
    $ \a -> Identity r -> Identity r
    k -> r -> Identity r
    forall a. a -> Identity a
    Identity (r -> Identity r) -> (Identity r -> r) -> Identity r -> Identity r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                             (a -> r -> r) -> r -> r
    forall r. (a -> r -> r) -> r -> r
    f (\a
    a -> Identity r -> r
    forall a. Identity a -> a
    runIdentity (Identity r -> r) -> (r -> Identity r) -> r -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Identity r -> Identity r
    k a
    a (Identity r -> Identity r) -> (r -> Identity r) -> r -> Identity r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . r -> Identity r
    forall a. a -> Identity a
    Identity) (r -> r) -> (Identity r -> r) -> Identity r -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                             Identity r -> r
    forall a. Identity a -> a
    runIdentity

    -------------------------------------------------------------------------
    -- | Extracts the first result from a 'Logic' computation, failing if
    -- there are no results.
    --
    -- >>> observe (pure 5 <|> pure 3 <|> empty)
    -- 5
    --
    -- >>> observe empty
    -- *** Exception: No answer.
    --
    -- Since 'Logic' is isomorphic to a list, 'observe' is analogous to 'head'.
    --
    observe :: Logic a -> a
    observe :: forall a. Logic a -> a
    observe Logic a
    lt = Identity a -> a
    forall a. Identity a -> a
    runIdentity (Identity a -> a) -> Identity a -> a
    forall a b. (a -> b) -> a -> b
    $ Logic a
    -> forall r.
       (a -> Identity r -> Identity r) -> Identity r -> Identity r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT Logic a
    lt (Identity a -> Identity a -> Identity a
    forall a b. a -> b -> a
    const (Identity a -> Identity a -> Identity a)
    -> (a -> Identity a) -> a -> Identity a -> Identity a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Identity a
    forall a. a -> Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure) (String -> Identity a
    forall a. HasCallStack => String -> a
    error String
    "No answer.")

    -------------------------------------------------------------------------
    -- | Extracts all results from a 'Logic' computation.
    --
    -- >>> observeAll (pure 5 <|> empty <|> empty <|> pure 3 <|> empty)
    -- [5,3]
    --
    -- 'observeAll' reveals a half of the isomorphism between 'Logic'
    -- and lists. See description of 'runLogic' for the other half.
    --
    observeAll :: Logic a -> [a]
    observeAll :: forall a. Logic a -> [a]
    observeAll = Identity [a] -> [a]
    forall a. Identity a -> a
    runIdentity (Identity [a] -> [a])
    -> (Logic a -> Identity [a]) -> Logic a -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Logic a -> Identity [a]
    forall (m :: * -> *) a. Applicative m => LogicT m a -> m [a]
    observeAllT

    -------------------------------------------------------------------------
    -- | Extracts up to a given number of results from a 'Logic' computation.
    --
    -- >>> let nats = pure 0 <|> fmap (+ 1) nats
    -- >>> observeMany 5 nats
    -- [0,1,2,3,4]
    --
    -- Since 'Logic' is isomorphic to a list, 'observeMany' is analogous to 'take'.
    --
    observeMany :: Int -> Logic a -> [a]
    observeMany :: forall a. Int -> Logic a -> [a]
    observeMany Int
    i = Int -> [a] -> [a]
    forall a. Int -> [a] -> [a]
    take Int
    i ([a] -> [a]) -> (Logic a -> [a]) -> Logic a -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Logic a -> [a]
    forall a. Logic a -> [a]
    observeAll
    -- Implementing 'observeMany' using 'observeManyT' is quite costly,
    -- because it calls 'msplit' multiple times.

    -------------------------------------------------------------------------
    -- | Runs a 'Logic' computation with the specified initial success and
    -- failure continuations.
    --
    -- >>> runLogic empty (+) 0
    -- 0
    --
    -- >>> runLogic (pure 5 <|> pure 3 <|> empty) (+) 0
    -- 8
    --
    -- When invoked with @(:)@ and @[]@ as arguments, reveals
    -- a half of the isomorphism between 'Logic' and lists.
    -- See description of 'observeAll' for the other half.
    --
    runLogic :: Logic a -> (a -> r -> r) -> r -> r
    runLogic :: forall a r. Logic a -> (a -> r -> r) -> r -> r
    runLogic Logic a
    l a -> r -> r
    s r
    f = Identity r -> r
    forall a. Identity a -> a
    runIdentity (Identity r -> r) -> Identity r -> r
    forall a b. (a -> b) -> a -> b
    $ Logic a
    -> forall r.
       (a -> Identity r -> Identity r) -> Identity r -> Identity r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT Logic a
    l a -> Identity r -> Identity r
    si Identity r
    fi
     where
     si :: a -> Identity r -> Identity r
    si = (r -> r) -> Identity r -> Identity r
    forall a b. (a -> b) -> Identity a -> Identity b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((r -> r) -> Identity r -> Identity r)
    -> (a -> r -> r) -> a -> Identity r -> Identity r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> r -> r
    s
     fi :: Identity r
    fi = r -> Identity r
    forall a. a -> Identity a
    Identity r
    f

    instance Functor (LogicT f) where
        fmap :: forall a b. (a -> b) -> LogicT f a -> LogicT f b
    fmap a -> b
    f LogicT f a
    lt = (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b)
    -> (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
    forall a b. (a -> b) -> a -> b
    $ \b -> f r -> f r
    sk f r
    fk -> LogicT f a -> forall r. (a -> f r -> f r) -> f r -> f r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT f a
    lt (b -> f r -> f r
    sk (b -> f r -> f r) -> (a -> b) -> a -> f r -> f r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b
    f) f r
    fk

    instance Applicative (LogicT f) where
        pure :: forall a. a -> LogicT f a
    pure a
    a = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
    -> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
    forall a b. (a -> b) -> a -> b
    $ \a -> f r -> f r
    sk f r
    fk -> a -> f r -> f r
    sk a
    a f r
    fk
        LogicT f (a -> b)
    f <*> :: forall a b. LogicT f (a -> b) -> LogicT f a -> LogicT f b
    <*> LogicT f a
    a = (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b)
    -> (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
    forall a b. (a -> b) -> a -> b
    $ \b -> f r -> f r
    sk f r
    fk -> LogicT f (a -> b)
    -> forall r. ((a -> b) -> f r -> f r) -> f r -> f r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT f (a -> b)
    f (\a -> b
    g f r
    fk' -> LogicT f a -> forall r. (a -> f r -> f r) -> f r -> f r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT f a
    a (b -> f r -> f r
    sk (b -> f r -> f r) -> (a -> b) -> a -> f r -> f r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b
    g) f r
    fk') f r
    fk

    instance Alternative (LogicT f) where
        empty :: forall a. LogicT f a
    empty = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
    -> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
    forall a b. (a -> b) -> a -> b
    $ \a -> f r -> f r
    _ f r
    fk -> f r
    fk
        LogicT f a
    f1 <|> :: forall a. LogicT f a -> LogicT f a -> LogicT f a
    <|> LogicT f a
    f2 = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
    -> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
    forall a b. (a -> b) -> a -> b
    $ \a -> f r -> f r
    sk f r
    fk -> LogicT f a -> forall r. (a -> f r -> f r) -> f r -> f r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT f a
    f1 a -> f r -> f r
    sk (LogicT f a -> forall r. (a -> f r -> f r) -> f r -> f r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT f a
    f2 a -> f r -> f r
    sk f r
    fk)

    instance Monad (LogicT m) where
        return :: forall a. a -> LogicT m a
    return = a -> LogicT m a
    forall a. a -> LogicT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
        LogicT m a
    m >>= :: forall a b. LogicT m a -> (a -> LogicT m b) -> LogicT m b
    >>= a -> LogicT m b
    f = (forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b)
    -> (forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b
    forall a b. (a -> b) -> a -> b
    $ \b -> m r -> m r
    sk m r
    fk -> LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    m (\a
    a m r
    fk' -> LogicT m b -> forall r. (b -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT (a -> LogicT m b
    f a
    a) b -> m r -> m r
    sk m r
    fk') m r
    fk
    #if !MIN_VERSION_base(4,13,0)
        fail = Fail.fail
    #endif

    instance Fail.MonadFail (LogicT m) where
        fail :: forall a. String -> LogicT m a
    fail String
    _ = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
    -> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall a b. (a -> b) -> a -> b
    $ \a -> m r -> m r
    _ m r
    fk -> m r
    fk

    instance MonadPlus (LogicT m) where
      mzero :: forall a. LogicT m a
    mzero = LogicT m a
    forall a. LogicT m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
      mplus :: forall a. LogicT m a -> LogicT m a -> LogicT m a
    mplus = LogicT m a -> LogicT m a -> LogicT m a
    forall a. LogicT m a -> LogicT m a -> LogicT m a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    (<|>)

    #if MIN_VERSION_base(4,9,0)
    instance Semigroup (LogicT m a) where
      <> :: LogicT m a -> LogicT m a -> LogicT m a
    (<>) = LogicT m a -> LogicT m a -> LogicT m a
    forall a. LogicT m a -> LogicT m a -> LogicT m a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus
      sconcat :: NonEmpty (LogicT m a) -> LogicT m a
    sconcat = (LogicT m a -> LogicT m a -> LogicT m a)
    -> NonEmpty (LogicT m a) -> LogicT m a
    forall a. (a -> a -> a) -> NonEmpty a -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 LogicT m a -> LogicT m a -> LogicT m a
    forall a. LogicT m a -> LogicT m a -> LogicT m a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus
    #endif

    instance Monoid (LogicT m a) where
      mempty :: LogicT m a
    mempty = LogicT m a
    forall a. LogicT m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
    #if MIN_VERSION_base(4,9,0)
      mappend :: LogicT m a -> LogicT m a -> LogicT m a
    mappend = LogicT m a -> LogicT m a -> LogicT m a
    forall a. Semigroup a => a -> a -> a
    (<>)
    #else
      mappend = (<|>)
    #endif
      mconcat :: [LogicT m a] -> LogicT m a
    mconcat = [LogicT m a] -> LogicT m a
    forall (t :: * -> *) (f :: * -> *) a.
    (Foldable t, Alternative f) =>
    t (f a) -> f a
    F.asum

    instance MonadTrans LogicT where
        lift :: forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    lift m a
    m = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
    -> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall a b. (a -> b) -> a -> b
    $ \a -> m r -> m r
    sk m r
    fk -> m a
    m m a -> (a -> m r) -> m r
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a
    a -> a -> m r -> m r
    sk a
    a m r
    fk

    instance (MonadIO m) => MonadIO (LogicT m) where
        liftIO :: forall a. IO a -> LogicT m a
    liftIO = m a -> LogicT m a
    forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m a -> LogicT m a) -> (IO a -> m a) -> IO a -> LogicT m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IO a -> m a
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO

    instance (Monad m) => MonadLogic (LogicT m) where
        -- 'msplit' is quite costly even if the base 'Monad' is 'Identity'.
        -- Try to avoid it.
        msplit :: forall a. LogicT m a -> LogicT m (Maybe (a, LogicT m a))
    msplit LogicT m a
    m = m (Maybe (a, LogicT m a)) -> LogicT m (Maybe (a, LogicT m a))
    forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m (Maybe (a, LogicT m a)) -> LogicT m (Maybe (a, LogicT m a)))
    -> m (Maybe (a, LogicT m a)) -> LogicT m (Maybe (a, LogicT m a))
    forall a b. (a -> b) -> a -> b
    $ LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    m a -> m (Maybe (a, LogicT m a)) -> m (Maybe (a, LogicT m a))
    forall {t :: (* -> *) -> * -> *} {m :: * -> *} {m :: * -> *} {a}
           {b}.
    (MonadTrans t, Monad m, Monad m, Monad (t m), Alternative (t m)) =>
    a -> m (Maybe (b, t m b)) -> m (Maybe (a, t m b))
    ssk (Maybe (a, LogicT m a) -> m (Maybe (a, LogicT m a))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (a, LogicT m a)
    forall a. Maybe a
    Nothing)
         where
         ssk :: a -> m (Maybe (b, t m b)) -> m (Maybe (a, t m b))
    ssk a
    a m (Maybe (b, t m b))
    fk = Maybe (a, t m b) -> m (Maybe (a, t m b))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (a, t m b) -> m (Maybe (a, t m b)))
    -> Maybe (a, t m b) -> m (Maybe (a, t m b))
    forall a b. (a -> b) -> a -> b
    $ (a, t m b) -> Maybe (a, t m b)
    forall a. a -> Maybe a
    Just (a
    a, m (Maybe (b, t m b)) -> t m (Maybe (b, t m b))
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m (Maybe (b, t m b))
    fk t m (Maybe (b, t m b)) -> (Maybe (b, t m b) -> t m b) -> t m b
    forall a b. t m a -> (a -> t m b) -> t m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Maybe (b, t m b) -> t m b
    forall (m :: * -> *) a. Alternative m => Maybe (a, m a) -> m a
    reflect)
        once :: forall a. LogicT m a -> LogicT m a
    once LogicT m a
    m = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
    -> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall a b. (a -> b) -> a -> b
    $ \a -> m r -> m r
    sk m r
    fk -> LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    m (\a
    a m r
    _ -> a -> m r -> m r
    sk a
    a m r
    fk) m r
    fk
        lnot :: forall a. LogicT m a -> LogicT m ()
    lnot LogicT m a
    m = (forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ()
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ())
    -> (forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ()
    forall a b. (a -> b) -> a -> b
    $ \() -> m r -> m r
    sk m r
    fk -> LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    m (\a
    _ m r
    _ -> m r
    fk) (() -> m r -> m r
    sk () m r
    fk)

    #if MIN_VERSION_base(4,8,0)

    instance {-# OVERLAPPABLE #-} (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where
        foldMap :: forall m a. Monoid m => (a -> m) -> LogicT m a -> m
    foldMap a -> m
    f LogicT m a
    m = m m -> m
    forall m. Monoid m => m m -> m
    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
    F.fold (m m -> m) -> m m -> m
    forall a b. (a -> b) -> a -> b
    $ LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    m ((m -> m) -> m m -> m m
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((m -> m) -> m m -> m m) -> (a -> m -> m) -> a -> m m -> m m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m -> m -> m
    forall a. Monoid a => a -> a -> a
    mappend (m -> m -> m) -> (a -> m) -> a -> m -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> m
    f) (m -> m m
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure m
    forall a. Monoid a => a
    mempty)

    instance {-# OVERLAPPING #-} F.Foldable (LogicT Identity) where
        foldr :: forall a b. (a -> b -> b) -> b -> LogicT Identity a -> b
    foldr a -> b -> b
    f b
    z LogicT Identity a
    m = LogicT Identity a -> (a -> b -> b) -> b -> b
    forall a r. Logic a -> (a -> r -> r) -> r -> r
    runLogic LogicT Identity a
    m a -> b -> b
    f b
    z

    #else

    instance (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where
        foldMap f m = F.fold $ unLogicT m (fmap . mappend . f) (pure mempty)

    #endif

    -- A much simpler logic monad representation used to define the Traversable and
    -- MonadZip instances. This is essentially the same as ListT from the list-t
    -- package, but it uses a slightly more efficient representation: MLView m a is
    -- more compact than Maybe (a, ML m a), and the additional laziness in the
    -- latter appears to be incidental/historical.
    newtype ML m a = ML (m (MLView m a))
      deriving ((forall a b. (a -> b) -> ML m a -> ML m b)
    -> (forall a b. a -> ML m b -> ML m a) -> Functor (ML m)
    forall a b. a -> ML m b -> ML m a
    forall a b. (a -> b) -> ML m a -> ML m b
    forall (m :: * -> *) a b. Functor m => a -> ML m b -> ML m a
    forall (m :: * -> *) a b. Functor m => (a -> b) -> ML m a -> ML m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall (m :: * -> *) a b. Functor m => (a -> b) -> ML m a -> ML m b
    fmap :: forall a b. (a -> b) -> ML m a -> ML m b
    $c<$ :: forall (m :: * -> *) a b. Functor m => a -> ML m b -> ML m a
    <$ :: forall a b. a -> ML m b -> ML m a
    Functor, (forall m. Monoid m => ML m m -> m)
    -> (forall m a. Monoid m => (a -> m) -> ML m a -> m)
    -> (forall m a. Monoid m => (a -> m) -> ML m a -> m)
    -> (forall a b. (a -> b -> b) -> b -> ML m a -> b)
    -> (forall a b. (a -> b -> b) -> b -> ML m a -> b)
    -> (forall b a. (b -> a -> b) -> b -> ML m a -> b)
    -> (forall b a. (b -> a -> b) -> b -> ML m a -> b)
    -> (forall a. (a -> a -> a) -> ML m a -> a)
    -> (forall a. (a -> a -> a) -> ML m a -> a)
    -> (forall a. ML m a -> [a])
    -> (forall a. ML m a -> Bool)
    -> (forall a. ML m a -> Int)
    -> (forall a. Eq a => a -> ML m a -> Bool)
    -> (forall a. Ord a => ML m a -> a)
    -> (forall a. Ord a => ML m a -> a)
    -> (forall a. Num a => ML m a -> a)
    -> (forall a. Num a => ML m a -> a)
    -> Foldable (ML m)
    forall a. Eq a => a -> ML m a -> Bool
    forall a. Num a => ML m a -> a
    forall a. Ord a => ML m a -> a
    forall m. Monoid m => ML m m -> m
    forall a. ML m a -> Bool
    forall a. ML m a -> Int
    forall a. ML m a -> [a]
    forall a. (a -> a -> a) -> ML m a -> a
    forall m a. Monoid m => (a -> m) -> ML m a -> m
    forall b a. (b -> a -> b) -> b -> ML m a -> b
    forall a b. (a -> b -> b) -> b -> ML m a -> b
    forall (m :: * -> *) a. (Foldable m, Eq a) => a -> ML m a -> Bool
    forall (m :: * -> *) a. (Foldable m, Num a) => ML m a -> a
    forall (m :: * -> *) a. (Foldable m, Ord a) => ML m a -> a
    forall (m :: * -> *) m. (Foldable m, Monoid m) => ML m m -> m
    forall (m :: * -> *) a. Foldable m => ML m a -> Bool
    forall (m :: * -> *) a. Foldable m => ML m a -> Int
    forall (m :: * -> *) a. Foldable m => ML m a -> [a]
    forall (m :: * -> *) a. Foldable m => (a -> a -> a) -> ML m a -> a
    forall (m :: * -> *) m a.
    (Foldable m, Monoid m) =>
    (a -> m) -> ML m a -> m
    forall (m :: * -> *) b a.
    Foldable m =>
    (b -> a -> b) -> b -> ML m a -> b
    forall (m :: * -> *) a b.
    Foldable m =>
    (a -> b -> b) -> b -> ML m a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall (m :: * -> *) m. (Foldable m, Monoid m) => ML m m -> m
    fold :: forall m. Monoid m => ML m m -> m
    $cfoldMap :: forall (m :: * -> *) m a.
    (Foldable m, Monoid m) =>
    (a -> m) -> ML m a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> ML m a -> m
    $cfoldMap' :: forall (m :: * -> *) m a.
    (Foldable m, Monoid m) =>
    (a -> m) -> ML m a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> ML m a -> m
    $cfoldr :: forall (m :: * -> *) a b.
    Foldable m =>
    (a -> b -> b) -> b -> ML m a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> ML m a -> b
    $cfoldr' :: forall (m :: * -> *) a b.
    Foldable m =>
    (a -> b -> b) -> b -> ML m a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> ML m a -> b
    $cfoldl :: forall (m :: * -> *) b a.
    Foldable m =>
    (b -> a -> b) -> b -> ML m a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> ML m a -> b
    $cfoldl' :: forall (m :: * -> *) b a.
    Foldable m =>
    (b -> a -> b) -> b -> ML m a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> ML m a -> b
    $cfoldr1 :: forall (m :: * -> *) a. Foldable m => (a -> a -> a) -> ML m a -> a
    foldr1 :: forall a. (a -> a -> a) -> ML m a -> a
    $cfoldl1 :: forall (m :: * -> *) a. Foldable m => (a -> a -> a) -> ML m a -> a
    foldl1 :: forall a. (a -> a -> a) -> ML m a -> a
    $ctoList :: forall (m :: * -> *) a. Foldable m => ML m a -> [a]
    toList :: forall a. ML m a -> [a]
    $cnull :: forall (m :: * -> *) a. Foldable m => ML m a -> Bool
    null :: forall a. ML m a -> Bool
    $clength :: forall (m :: * -> *) a. Foldable m => ML m a -> Int
    length :: forall a. ML m a -> Int
    $celem :: forall (m :: * -> *) a. (Foldable m, Eq a) => a -> ML m a -> Bool
    elem :: forall a. Eq a => a -> ML m a -> Bool
    $cmaximum :: forall (m :: * -> *) a. (Foldable m, Ord a) => ML m a -> a
    maximum :: forall a. Ord a => ML m a -> a
    $cminimum :: forall (m :: * -> *) a. (Foldable m, Ord a) => ML m a -> a
    minimum :: forall a. Ord a => ML m a -> a
    $csum :: forall (m :: * -> *) a. (Foldable m, Num a) => ML m a -> a
    sum :: forall a. Num a => ML m a -> a
    $cproduct :: forall (m :: * -> *) a. (Foldable m, Num a) => ML m a -> a
    product :: forall a. Num a => ML m a -> a
    F.Foldable, Functor (ML m)
    Foldable (ML m)
    Functor (ML m)
    -> Foldable (ML m)
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> ML m a -> f (ML m b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        ML m (f a) -> f (ML m a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> ML m a -> m (ML m b))
    -> (forall (m :: * -> *) a. Monad m => ML m (m a) -> m (ML m a))
    -> Traversable (ML m)
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall {m :: * -> *}. Traversable m => Functor (ML m)
    forall {m :: * -> *}. Traversable m => Foldable (ML m)
    forall (m :: * -> *) (m :: * -> *) a.
    (Traversable m, Monad m) =>
    ML m (m a) -> m (ML m a)
    forall (m :: * -> *) (f :: * -> *) a.
    (Traversable m, Applicative f) =>
    ML m (f a) -> f (ML m a)
    forall (m :: * -> *) (m :: * -> *) a b.
    (Traversable m, Monad m) =>
    (a -> m b) -> ML m a -> m (ML m b)
    forall (m :: * -> *) (f :: * -> *) a b.
    (Traversable m, Applicative f) =>
    (a -> f b) -> ML m a -> f (ML m b)
    forall (m :: * -> *) a. Monad m => ML m (m a) -> m (ML m a)
    forall (f :: * -> *) a. Applicative f => ML m (f a) -> f (ML m a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ML m a -> m (ML m b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ML m a -> f (ML m b)
    $ctraverse :: forall (m :: * -> *) (f :: * -> *) a b.
    (Traversable m, Applicative f) =>
    (a -> f b) -> ML m a -> f (ML m b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ML m a -> f (ML m b)
    $csequenceA :: forall (m :: * -> *) (f :: * -> *) a.
    (Traversable m, Applicative f) =>
    ML m (f a) -> f (ML m a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => ML m (f a) -> f (ML m a)
    $cmapM :: forall (m :: * -> *) (m :: * -> *) a b.
    (Traversable m, Monad m) =>
    (a -> m b) -> ML m a -> m (ML m b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ML m a -> m (ML m b)
    $csequence :: forall (m :: * -> *) (m :: * -> *) a.
    (Traversable m, Monad m) =>
    ML m (m a) -> m (ML m a)
    sequence :: forall (m :: * -> *) a. Monad m => ML m (m a) -> m (ML m a)
    T.Traversable)

    data MLView m a = EmptyML | ConsML a (ML m a)
      deriving ((forall a b. (a -> b) -> MLView m a -> MLView m b)
    -> (forall a b. a -> MLView m b -> MLView m a)
    -> Functor (MLView m)
    forall a b. a -> MLView m b -> MLView m a
    forall a b. (a -> b) -> MLView m a -> MLView m b
    forall (m :: * -> *) a b.
    Functor m =>
    a -> MLView m b -> MLView m a
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> MLView m a -> MLView m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> MLView m a -> MLView m b
    fmap :: forall a b. (a -> b) -> MLView m a -> MLView m b
    $c<$ :: forall (m :: * -> *) a b.
    Functor m =>
    a -> MLView m b -> MLView m a
    <$ :: forall a b. a -> MLView m b -> MLView m a
    Functor, (forall m. Monoid m => MLView m m -> m)
    -> (forall m a. Monoid m => (a -> m) -> MLView m a -> m)
    -> (forall m a. Monoid m => (a -> m) -> MLView m a -> m)
    -> (forall a b. (a -> b -> b) -> b -> MLView m a -> b)
    -> (forall a b. (a -> b -> b) -> b -> MLView m a -> b)
    -> (forall b a. (b -> a -> b) -> b -> MLView m a -> b)
    -> (forall b a. (b -> a -> b) -> b -> MLView m a -> b)
    -> (forall a. (a -> a -> a) -> MLView m a -> a)
    -> (forall a. (a -> a -> a) -> MLView m a -> a)
    -> (forall a. MLView m a -> [a])
    -> (forall a. MLView m a -> Bool)
    -> (forall a. MLView m a -> Int)
    -> (forall a. Eq a => a -> MLView m a -> Bool)
    -> (forall a. Ord a => MLView m a -> a)
    -> (forall a. Ord a => MLView m a -> a)
    -> (forall a. Num a => MLView m a -> a)
    -> (forall a. Num a => MLView m a -> a)
    -> Foldable (MLView m)
    forall a. Eq a => a -> MLView m a -> Bool
    forall a. Num a => MLView m a -> a
    forall a. Ord a => MLView m a -> a
    forall m. Monoid m => MLView m m -> m
    forall a. MLView m a -> Bool
    forall a. MLView m a -> Int
    forall a. MLView m a -> [a]
    forall a. (a -> a -> a) -> MLView m a -> a
    forall m a. Monoid m => (a -> m) -> MLView m a -> m
    forall b a. (b -> a -> b) -> b -> MLView m a -> b
    forall a b. (a -> b -> b) -> b -> MLView m a -> b
    forall (m :: * -> *) a.
    (Foldable m, Eq a) =>
    a -> MLView m a -> Bool
    forall (m :: * -> *) a. (Foldable m, Num a) => MLView m a -> a
    forall (m :: * -> *) a. (Foldable m, Ord a) => MLView m a -> a
    forall (m :: * -> *) m. (Foldable m, Monoid m) => MLView m m -> m
    forall (m :: * -> *) a. Foldable m => MLView m a -> Bool
    forall (m :: * -> *) a. Foldable m => MLView m a -> Int
    forall (m :: * -> *) a. Foldable m => MLView m a -> [a]
    forall (m :: * -> *) a.
    Foldable m =>
    (a -> a -> a) -> MLView m a -> a
    forall (m :: * -> *) m a.
    (Foldable m, Monoid m) =>
    (a -> m) -> MLView m a -> m
    forall (m :: * -> *) b a.
    Foldable m =>
    (b -> a -> b) -> b -> MLView m a -> b
    forall (m :: * -> *) a b.
    Foldable m =>
    (a -> b -> b) -> b -> MLView m a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall (m :: * -> *) m. (Foldable m, Monoid m) => MLView m m -> m
    fold :: forall m. Monoid m => MLView m m -> m
    $cfoldMap :: forall (m :: * -> *) m a.
    (Foldable m, Monoid m) =>
    (a -> m) -> MLView m a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> MLView m a -> m
    $cfoldMap' :: forall (m :: * -> *) m a.
    (Foldable m, Monoid m) =>
    (a -> m) -> MLView m a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> MLView m a -> m
    $cfoldr :: forall (m :: * -> *) a b.
    Foldable m =>
    (a -> b -> b) -> b -> MLView m a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> MLView m a -> b
    $cfoldr' :: forall (m :: * -> *) a b.
    Foldable m =>
    (a -> b -> b) -> b -> MLView m a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> MLView m a -> b
    $cfoldl :: forall (m :: * -> *) b a.
    Foldable m =>
    (b -> a -> b) -> b -> MLView m a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> MLView m a -> b
    $cfoldl' :: forall (m :: * -> *) b a.
    Foldable m =>
    (b -> a -> b) -> b -> MLView m a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> MLView m a -> b
    $cfoldr1 :: forall (m :: * -> *) a.
    Foldable m =>
    (a -> a -> a) -> MLView m a -> a
    foldr1 :: forall a. (a -> a -> a) -> MLView m a -> a
    $cfoldl1 :: forall (m :: * -> *) a.
    Foldable m =>
    (a -> a -> a) -> MLView m a -> a
    foldl1 :: forall a. (a -> a -> a) -> MLView m a -> a
    $ctoList :: forall (m :: * -> *) a. Foldable m => MLView m a -> [a]
    toList :: forall a. MLView m a -> [a]
    $cnull :: forall (m :: * -> *) a. Foldable m => MLView m a -> Bool
    null :: forall a. MLView m a -> Bool
    $clength :: forall (m :: * -> *) a. Foldable m => MLView m a -> Int
    length :: forall a. MLView m a -> Int
    $celem :: forall (m :: * -> *) a.
    (Foldable m, Eq a) =>
    a -> MLView m a -> Bool
    elem :: forall a. Eq a => a -> MLView m a -> Bool
    $cmaximum :: forall (m :: * -> *) a. (Foldable m, Ord a) => MLView m a -> a
    maximum :: forall a. Ord a => MLView m a -> a
    $cminimum :: forall (m :: * -> *) a. (Foldable m, Ord a) => MLView m a -> a
    minimum :: forall a. Ord a => MLView m a -> a
    $csum :: forall (m :: * -> *) a. (Foldable m, Num a) => MLView m a -> a
    sum :: forall a. Num a => MLView m a -> a
    $cproduct :: forall (m :: * -> *) a. (Foldable m, Num a) => MLView m a -> a
    product :: forall a. Num a => MLView m a -> a
    F.Foldable)

    instance T.Traversable m => T.Traversable (MLView m) where
      traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> MLView m a -> f (MLView m b)
    traverse a -> f b
    _ MLView m a
    EmptyML = MLView m b -> f (MLView m b)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure MLView m b
    forall (m :: * -> *) a. MLView m a
    EmptyML
      traverse a -> f b
    f (ConsML a
    x (ML m (MLView m a)
    m))
        = (b -> m (MLView m b) -> MLView m b)
    -> f b -> f (m (MLView m b)) -> f (MLView m b)
    forall a b c. (a -> b -> c) -> f a -> f b -> f c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (\b
    y m (MLView m b)
    ym -> b -> ML m b -> MLView m b
    forall (m :: * -> *) a. a -> ML m a -> MLView m a
    ConsML b
    y (m (MLView m b) -> ML m b
    forall (m :: * -> *) a. m (MLView m a) -> ML m a
    ML m (MLView m b)
    ym)) (a -> f b
    f a
    x) ((MLView m a -> f (MLView m b))
    -> m (MLView m a) -> f (m (MLView m b))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> m a -> f (m b)
    T.traverse ((a -> f b) -> MLView m a -> f (MLView m b)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> MLView m a -> f (MLView m b)
    T.traverse a -> f b
    f) m (MLView m a)
    m)
      {- The derived instance would write the second case as
       -
       -   traverse f (ConsML x xs) = liftA2 ConsML (f x) (traverse @(ML m) f xs)
       -
       - Inlining the inner traverse gives
       -
       -   traverse f (ConsML x (ML m)) = liftA2 ConsML (f x) (ML <$> traverse (traverse f) m)
       -
       - revealing fmap under liftA2. We fuse those into a single application of liftA2,
       - in case fmap isn't free.
      -}

    toML :: Applicative m => LogicT m a -> ML m a
    toML :: forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
    toML (LogicT forall r. (a -> m r -> m r) -> m r -> m r
    q) = m (MLView m a) -> ML m a
    forall (m :: * -> *) a. m (MLView m a) -> ML m a
    ML (m (MLView m a) -> ML m a) -> m (MLView m a) -> ML m a
    forall a b. (a -> b) -> a -> b
    $ (a -> m (MLView m a) -> m (MLView m a))
    -> m (MLView m a) -> m (MLView m a)
    forall r. (a -> m r -> m r) -> m r -> m r
    q (\a
    a m (MLView m a)
    m -> MLView m a -> m (MLView m a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (MLView m a -> m (MLView m a)) -> MLView m a -> m (MLView m a)
    forall a b. (a -> b) -> a -> b
    $ a -> ML m a -> MLView m a
    forall (m :: * -> *) a. a -> ML m a -> MLView m a
    ConsML a
    a (m (MLView m a) -> ML m a
    forall (m :: * -> *) a. m (MLView m a) -> ML m a
    ML m (MLView m a)
    m)) (MLView m a -> m (MLView m a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure MLView m a
    forall (m :: * -> *) a. MLView m a
    EmptyML)

    fromML :: Monad m => ML m a -> LogicT m a
    fromML :: forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
    fromML (ML m (MLView m a)
    m) = m (MLView m a) -> LogicT m (MLView m a)
    forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m (MLView m a)
    m LogicT m (MLView m a) -> (MLView m a -> LogicT m a) -> LogicT m a
    forall a b. LogicT m a -> (a -> LogicT m b) -> LogicT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \MLView m a
    r -> case MLView m a
    r of
      MLView m a
    EmptyML -> LogicT m a
    forall a. LogicT m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
      ConsML a
    a ML m a
    xs -> a -> LogicT m a
    forall a. a -> LogicT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    a LogicT m a -> LogicT m a -> LogicT m a
    forall a. LogicT m a -> LogicT m a -> LogicT m a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> ML m a -> LogicT m a
    forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
    fromML ML m a
    xs

    #if MIN_VERSION_base(4,8,0)
    instance {-# OVERLAPPING #-} T.Traversable (LogicT Identity) where
      traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LogicT Identity a -> f (LogicT Identity b)
    traverse a -> f b
    g LogicT Identity a
    l = LogicT Identity a
    -> (a -> f (LogicT Identity b) -> f (LogicT Identity b))
    -> f (LogicT Identity b)
    -> f (LogicT Identity b)
    forall a r. Logic a -> (a -> r -> r) -> r -> r
    runLogic LogicT Identity a
    l (\a
    a f (LogicT Identity b)
    ft -> b -> LogicT Identity b -> LogicT Identity b
    forall {f :: * -> *} {a}. Alternative f => a -> f a -> f a
    cons (b -> LogicT Identity b -> LogicT Identity b)
    -> f b -> f (LogicT Identity b -> LogicT Identity b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> f b
    g a
    a f (LogicT Identity b -> LogicT Identity b)
    -> f (LogicT Identity b) -> f (LogicT Identity b)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f (LogicT Identity b)
    ft) (LogicT Identity b -> f (LogicT Identity b)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LogicT Identity b
    forall a. LogicT Identity a
    forall (f :: * -> *) a. Alternative f => f a
    empty)
        where
          cons :: a -> f a -> f a
    cons a
    a f a
    l' = a -> f a
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    a f a -> f a -> f a
    forall a. f a -> f a -> f a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> f a
    l'
    instance {-# OVERLAPPABLE #-} (Monad m, T.Traversable m) => T.Traversable (LogicT m) where
      traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> LogicT m a -> f (LogicT m b)
    traverse a -> f b
    f = (ML m b -> LogicT m b) -> f (ML m b) -> f (LogicT m b)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ML m b -> LogicT m b
    forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
    fromML (f (ML m b) -> f (LogicT m b))
    -> (LogicT m a -> f (ML m b)) -> LogicT m a -> f (LogicT m b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> f b) -> ML m a -> f (ML m b)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ML m a -> f (ML m b)
    T.traverse a -> f b
    f (ML m a -> f (ML m b))
    -> (LogicT m a -> ML m a) -> LogicT m a -> f (ML m b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LogicT m a -> ML m a
    forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
    toML
    #else
    instance (Monad m, Applicative m, T.Traversable m) => T.Traversable (LogicT m) where
      traverse f = fmap fromML . T.traverse f . toML
    #endif

    #if MIN_VERSION_base(4,8,0)
    zipWithML :: MonadZip m => (a -> b -> c) -> ML m a -> ML m b -> ML m c
    zipWithML :: forall (m :: * -> *) a b c.
    MonadZip m =>
    (a -> b -> c) -> ML m a -> ML m b -> ML m c
    zipWithML a -> b -> c
    f = ML m a -> ML m b -> ML m c
    forall {m :: * -> *}. MonadZip m => ML m a -> ML m b -> ML m c
    go
        where
          go :: ML m a -> ML m b -> ML m c
    go (ML m (MLView m a)
    m1) (ML m (MLView m b)
    m2) =
            m (MLView m c) -> ML m c
    forall (m :: * -> *) a. m (MLView m a) -> ML m a
    ML (m (MLView m c) -> ML m c) -> m (MLView m c) -> ML m c
    forall a b. (a -> b) -> a -> b
    $ (MLView m a -> MLView m b -> MLView m c)
    -> m (MLView m a) -> m (MLView m b) -> m (MLView m c)
    forall a b c. (a -> b -> c) -> m a -> m b -> m c
    forall (m :: * -> *) a b c.
    MonadZip m =>
    (a -> b -> c) -> m a -> m b -> m c
    mzipWith MLView m a -> MLView m b -> MLView m c
    zv m (MLView m a)
    m1 m (MLView m b)
    m2
          zv :: MLView m a -> MLView m b -> MLView m c
    zv (a
    a `ConsML` ML m a
    as) (b
    b `ConsML` ML m b
    bs) = a -> b -> c
    f a
    a b
    b c -> ML m c -> MLView m c
    forall (m :: * -> *) a. a -> ML m a -> MLView m a
    `ConsML` ML m a -> ML m b -> ML m c
    go ML m a
    as ML m b
    bs
          zv MLView m a
    _ MLView m b
    _ = MLView m c
    forall (m :: * -> *) a. MLView m a
    EmptyML

    unzipML :: MonadZip m => ML m (a, b) -> (ML m a, ML m b)
    unzipML :: forall (m :: * -> *) a b.
    MonadZip m =>
    ML m (a, b) -> (ML m a, ML m b)
    unzipML (ML m (MLView m (a, b))
    m)
        | (m (MLView m a)
    l, m (MLView m b)
    r) <- m (MLView m a, MLView m b) -> (m (MLView m a), m (MLView m b))
    forall a b. m (a, b) -> (m a, m b)
    forall (m :: * -> *) a b. MonadZip m => m (a, b) -> (m a, m b)
    munzip ((MLView m (a, b) -> (MLView m a, MLView m b))
    -> m (MLView m (a, b)) -> m (MLView m a, MLView m b)
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap MLView m (a, b) -> (MLView m a, MLView m b)
    forall {m :: * -> *} {a} {a}.
    MonadZip m =>
    MLView m (a, a) -> (MLView m a, MLView m a)
    go m (MLView m (a, b))
    m)
        = (m (MLView m a) -> ML m a
    forall (m :: * -> *) a. m (MLView m a) -> ML m a
    ML m (MLView m a)
    l, m (MLView m b) -> ML m b
    forall (m :: * -> *) a. m (MLView m a) -> ML m a
    ML m (MLView m b)
    r)
        where
          go :: MLView m (a, a) -> (MLView m a, MLView m a)
    go MLView m (a, a)
    EmptyML = (MLView m a
    forall (m :: * -> *) a. MLView m a
    EmptyML, MLView m a
    forall (m :: * -> *) a. MLView m a
    EmptyML)
          go ((a
    a, a
    b) `ConsML` ML m (a, a)
    listab)
            = (a
    a a -> ML m a -> MLView m a
    forall (m :: * -> *) a. a -> ML m a -> MLView m a
    `ConsML` ML m a
    la, a
    b a -> ML m a -> MLView m a
    forall (m :: * -> *) a. a -> ML m a -> MLView m a
    `ConsML` ML m a
    lb)
            where
              -- If the underlying munzip is careful not to leak memory, then we
              -- don't want to defeat it. We need to be sure that la and lb are
              -- realized as selector thunks. Hopefully the CPSish conversion
              -- doesn't muck anything up at another level.
              {-# NOINLINE remains #-}
              {-# NOINLINE la #-}
              {-# NOINLINE lb #-}
              remains :: (ML m a, ML m a)
    remains = ML m (a, a) -> (ML m a, ML m a)
    forall (m :: * -> *) a b.
    MonadZip m =>
    ML m (a, b) -> (ML m a, ML m b)
    unzipML ML m (a, a)
    listab
              (ML m a
    la, ML m a
    lb) = (ML m a, ML m a)
    remains

    instance MonadZip m => MonadZip (LogicT m) where
      mzipWith :: forall a b c.
    (a -> b -> c) -> LogicT m a -> LogicT m b -> LogicT m c
    mzipWith a -> b -> c
    f LogicT m a
    xs LogicT m b
    ys = ML m c -> LogicT m c
    forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
    fromML (ML m c -> LogicT m c) -> ML m c -> LogicT m c
    forall a b. (a -> b) -> a -> b
    $ (a -> b -> c) -> ML m a -> ML m b -> ML m c
    forall (m :: * -> *) a b c.
    MonadZip m =>
    (a -> b -> c) -> ML m a -> ML m b -> ML m c
    zipWithML a -> b -> c
    f (LogicT m a -> ML m a
    forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
    toML LogicT m a
    xs) (LogicT m b -> ML m b
    forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
    toML LogicT m b
    ys)
      munzip :: forall a b. LogicT m (a, b) -> (LogicT m a, LogicT m b)
    munzip LogicT m (a, b)
    xys = case ML m (a, b) -> (ML m a, ML m b)
    forall (m :: * -> *) a b.
    MonadZip m =>
    ML m (a, b) -> (ML m a, ML m b)
    unzipML (LogicT m (a, b) -> ML m (a, b)
    forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
    toML LogicT m (a, b)
    xys) of
        (ML m a
    xs, ML m b
    ys) -> (ML m a -> LogicT m a
    forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
    fromML ML m a
    xs, ML m b -> LogicT m b
    forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
    fromML ML m b
    ys)
    #endif

    -- Needs undecidable instances
    instance MonadReader r m => MonadReader r (LogicT m) where
        ask :: LogicT m r
    ask = m r -> LogicT m r
    forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m r
    forall r (m :: * -> *). MonadReader r m => m r
    ask
        local :: forall a. (r -> r) -> LogicT m a -> LogicT m a
    local r -> r
    f (LogicT forall r. (a -> m r -> m r) -> m r -> m r
    m) = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
    -> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall a b. (a -> b) -> a -> b
    $ \a -> m r -> m r
    sk m r
    fk -> do
            r
    env <- m r
    forall r (m :: * -> *). MonadReader r m => m r
    ask
            (r -> r) -> m r -> m r
    forall a. (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local r -> r
    f (m r -> m r) -> m r -> m r
    forall a b. (a -> b) -> a -> b
    $ (a -> m r -> m r) -> m r -> m r
    forall r. (a -> m r -> m r) -> m r -> m r
    m (((r -> r) -> m r -> m r
    forall a. (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (r -> r -> r
    forall a b. a -> b -> a
    const r
    env) (m r -> m r) -> (m r -> m r) -> m r -> m r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) ((m r -> m r) -> m r -> m r)
    -> (a -> m r -> m r) -> a -> m r -> m r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> m r -> m r
    sk) ((r -> r) -> m r -> m r
    forall a. (r -> r) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (r -> r -> r
    forall a b. a -> b -> a
    const r
    env) m r
    fk)

    -- Needs undecidable instances
    instance MonadState s m => MonadState s (LogicT m) where
        get :: LogicT m s
    get = m s -> LogicT m s
    forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m s
    forall s (m :: * -> *). MonadState s m => m s
    get
        put :: s -> LogicT m ()
    put = m () -> LogicT m ()
    forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> LogicT m ()) -> (s -> m ()) -> s -> LogicT m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . s -> m ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put

    -- Needs undecidable instances
    instance MonadError e m => MonadError e (LogicT m) where
      throwError :: forall a. e -> LogicT m a
    throwError = m a -> LogicT m a
    forall (m :: * -> *) a. Monad m => m a -> LogicT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m a -> LogicT m a) -> (e -> m a) -> e -> LogicT m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . e -> m a
    forall a. e -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError
      catchError :: forall a. LogicT m a -> (e -> LogicT m a) -> LogicT m a
    catchError LogicT m a
    m e -> LogicT m a
    h = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall (m :: * -> *) a.
    (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
    -> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
    forall a b. (a -> b) -> a -> b
    $ \a -> m r -> m r
    sk m r
    fk -> let
          handle :: m r -> m r
    handle m r
    r = m r
    r m r -> (e -> m r) -> m r
    forall a. m a -> (e -> m a) -> m a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \e
    e -> LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT (e -> LogicT m a
    h e
    e) a -> m r -> m r
    sk m r
    fk
        in m r -> m r
    handle (m r -> m r) -> m r -> m r
    forall a b. (a -> b) -> a -> b
    $ LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    forall (m :: * -> *) a.
    LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
    unLogicT LogicT m a
    m (\a
    a -> a -> m r -> m r
    sk a
    a (m r -> m r) -> (m r -> m r) -> m r -> m r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m r -> m r
    handle) m r
    fk