    {-# LANGUAGE CPP  #-}
    {-# LANGUAGE UndecidableInstances  #-} -- Due MonadReader/MonadState fundep

    -- | @ListT@ done right,
    --   see https://www.haskell.org/haskellwiki/ListT_done_right_alternative
    --
    --   There is also the @list-t@ package on hackage (Nikita Volkov)
    --   but it again depends on other packages we do not use yet,
    --   so we rather implement the few bits we need afresh.

    module Agda.Utils.ListT where

    import Control.Applicative ( Alternative((<|>), empty) )
    import Control.Monad
    import Control.Monad.Fail as Fail
    import Control.Monad.Reader
    import Control.Monad.State
    import Control.Monad.IO.Class ( MonadIO(..) )

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

    import Agda.Utils.Maybe
    import Agda.Utils.Monad

    -- | Lazy monadic computation of a list of results.
    newtype ListT m a = ListT { forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
    runListT :: m (Maybe (a, ListT m a)) }
      deriving ((forall a b. (a -> b) -> ListT m a -> ListT m b)
    -> (forall a b. a -> ListT m b -> ListT m a) -> Functor (ListT m)
    forall a b. a -> ListT m b -> ListT m a
    forall a b. (a -> b) -> ListT m a -> ListT m b
    forall (m :: * -> *) a b. Functor m => a -> ListT m b -> ListT m a
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> ListT m a -> ListT m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> ListT m b -> ListT m a
    $c<$ :: forall (m :: * -> *) a b. Functor m => a -> ListT m b -> ListT m a
    fmap :: forall a b. (a -> b) -> ListT m a -> ListT m b
    $cfmap :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> ListT m a -> ListT m b
    Functor)

    -- | Boilerplate function to lift 'MonadReader' through the 'ListT' transformer.
    mapListT :: (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))) -> ListT m a -> ListT n b
    mapListT :: forall (m :: * -> *) a (n :: * -> *) b.
    (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
    -> ListT m a -> ListT n b
    mapListT m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
    f = n (Maybe (b, ListT n b)) -> ListT n b
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (n (Maybe (b, ListT n b)) -> ListT n b)
    -> (ListT m a -> n (Maybe (b, ListT n b)))
    -> ListT m a
    -> ListT n b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
    f (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
    -> (ListT m a -> m (Maybe (a, ListT m a)))
    -> ListT m a
    -> n (Maybe (b, ListT n b))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ListT m a -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
    runListT

    -- | Inverse to 'mapListT'.
    unmapListT :: (ListT m a -> ListT n b) -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
    unmapListT :: forall (m :: * -> *) a (n :: * -> *) b.
    (ListT m a -> ListT n b)
    -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
    unmapListT ListT m a -> ListT n b
    f = ListT n b -> n (Maybe (b, ListT n b))
    forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
    runListT (ListT n b -> n (Maybe (b, ListT n b)))
    -> (m (Maybe (a, ListT m a)) -> ListT n b)
    -> m (Maybe (a, ListT m a))
    -> n (Maybe (b, ListT n b))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ListT m a -> ListT n b
    f (ListT m a -> ListT n b)
    -> (m (Maybe (a, ListT m a)) -> ListT m a)
    -> m (Maybe (a, ListT m a))
    -> ListT n b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (Maybe (a, ListT m a)) -> ListT m a
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT

    -- * List operations

    -- | The empty lazy list.
    nilListT :: Monad m => ListT m a
    nilListT :: forall (m :: * -> *) a. Monad m => ListT m a
    nilListT = m (Maybe (a, ListT m a)) -> ListT m a
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (m (Maybe (a, ListT m a)) -> ListT m a)
    -> m (Maybe (a, ListT m a)) -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (a, ListT m a)
    forall a. Maybe a
    Nothing

    -- | Consing a value to a lazy list.
    consListT :: Monad m => a -> ListT m a -> ListT m a
    consListT :: forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
    consListT a
    a ListT m a
    l = m (Maybe (a, ListT m a)) -> ListT m a
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (m (Maybe (a, ListT m a)) -> ListT m a)
    -> m (Maybe (a, ListT m a)) -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (a, ListT m a) -> m (Maybe (a, ListT m a)))
    -> Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
    forall a b. (a -> b) -> a -> b
    $ (a, ListT m a) -> Maybe (a, ListT m a)
    forall a. a -> Maybe a
    Just (a
    a, ListT m a
    l)

    -- | Singleton lazy list.
    sgListT ::  Monad m => a -> ListT m a
    sgListT :: forall (m :: * -> *) a. Monad m => a -> ListT m a
    sgListT a
    a = a -> ListT m a -> ListT m a
    forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
    consListT a
    a ListT m a
    forall (m :: * -> *) a. Monad m => ListT m a
    nilListT

    -- | Case distinction over lazy list.
    caseListT :: Monad m => ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
    caseListT :: forall (m :: * -> *) a b.
    Monad m =>
    ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
    caseListT ListT m a
    l m b
    nil a -> ListT m a -> m b
    cons = m (Maybe (a, ListT m a)) -> m b -> ((a, ListT m a) -> m b) -> m b
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (ListT m a -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
    runListT ListT m a
    l) m b
    nil (((a, ListT m a) -> m b) -> m b) -> ((a, ListT m a) -> m b) -> m b
    forall a b. (a -> b) -> a -> b
    $ (a -> ListT m a -> m b) -> (a, ListT m a) -> m b
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry a -> ListT m a -> m b
    cons

    -- | Folding a lazy list, effects left-to-right.
    foldListT :: Monad m => (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT a -> m b -> m b
    cons m b
    nil = ListT m a -> m b
    loop where
      loop :: ListT m a -> m b
    loop ListT m a
    l = ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
    forall (m :: * -> *) a b.
    Monad m =>
    ListT m a -> m b -> (a -> ListT m a -> m b) -> m b
    caseListT ListT m a
    l m b
    nil ((a -> ListT m a -> m b) -> m b) -> (a -> ListT m a -> m b) -> m b
    forall a b. (a -> b) -> a -> b
    $ \ a
    a ListT m a
    l' -> a -> m b -> m b
    cons a
    a (m b -> m b) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $ ListT m a -> m b
    loop ListT m a
    l'

    -- | Lazy monadic disjunction of lazy monadic list, effects left-to-right
    anyListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool
    anyListT :: forall (m :: * -> *) a.
    Monad m =>
    ListT m a -> (a -> m Bool) -> m Bool
    anyListT ListT m a
    xs a -> m Bool
    f = (a -> m Bool -> m Bool) -> m Bool -> ListT m a -> m Bool
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT (m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    or2M (m Bool -> m Bool -> m Bool)
    -> (a -> m Bool) -> a -> m Bool -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> m Bool
    f) (Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False) ListT m a
    xs

    -- | Lazy monadic conjunction of lazy monadic list, effects left-to-right
    allListT :: Monad m => ListT m a -> (a -> m Bool) -> m Bool
    allListT :: forall (m :: * -> *) a.
    Monad m =>
    ListT m a -> (a -> m Bool) -> m Bool
    allListT ListT m a
    xs a -> m Bool
    f = (a -> m Bool -> m Bool) -> m Bool -> ListT m a -> m Bool
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT (m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    and2M (m Bool -> m Bool -> m Bool)
    -> (a -> m Bool) -> a -> m Bool -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> m Bool
    f) (Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True) ListT m a
    xs

    -- | Force all values in the lazy list, effects left-to-right
    sequenceListT :: Monad m => ListT m a -> m [a]
    sequenceListT :: forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
    sequenceListT = (a -> m [a] -> m [a]) -> m [a] -> ListT m a -> m [a]
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT (([a] -> [a]) -> m [a] -> m [a]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    (<$>) (([a] -> [a]) -> m [a] -> m [a])
    -> (a -> [a] -> [a]) -> a -> m [a] -> m [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (:)) (m [a] -> ListT m a -> m [a]) -> m [a] -> ListT m a -> m [a]
    forall a b. (a -> b) -> a -> b
    $ [a] -> m [a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []

    -- | The join operation of the @ListT m@ monad.
    concatListT :: Monad m => ListT m (ListT m a) -> ListT m a
    concatListT :: forall (m :: * -> *) a. Monad m => ListT m (ListT m a) -> ListT m a
    concatListT = m (Maybe (a, ListT m a)) -> ListT m a
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (m (Maybe (a, ListT m a)) -> ListT m a)
    -> (ListT m (ListT m a) -> m (Maybe (a, ListT m a)))
    -> ListT m (ListT m a)
    -> ListT m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ListT m a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
    -> m (Maybe (a, ListT m a))
    -> ListT m (ListT m a)
    -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT ((ListT m a -> ListT m a)
    -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a (n :: * -> *) b.
    (ListT m a -> ListT n b)
    -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
    unmapListT ((ListT m a -> ListT m a)
     -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
    -> (ListT m a -> ListT m a -> ListT m a)
    -> ListT m a
    -> m (Maybe (a, ListT m a))
    -> m (Maybe (a, ListT m a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ListT m a -> ListT m a -> ListT m a
    forall a. Monoid a => a -> a -> a
    mappend) (Maybe (a, ListT m a) -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (a, ListT m a)
    forall a. Maybe a
    Nothing)

    -- * Monadic list operations.

    -- | We can ``run'' a computation of a 'ListT' as it is monadic itself.
    runMListT :: Monad m => m (ListT m a) -> ListT m a
    runMListT :: forall (m :: * -> *) a. Monad m => m (ListT m a) -> ListT m a
    runMListT m (ListT m a)
    ml = m (Maybe (a, ListT m a)) -> ListT m a
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (m (Maybe (a, ListT m a)) -> ListT m a)
    -> m (Maybe (a, ListT m a)) -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ ListT m a -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
    runListT (ListT m a -> m (Maybe (a, ListT m a)))
    -> m (ListT m a) -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m (ListT m a)
    ml

    -- | Monadic cons.
    consMListT :: Monad m => m a -> ListT m a -> ListT m a
    consMListT :: forall (m :: * -> *) a. Monad m => m a -> ListT m a -> ListT m a
    consMListT m a
    ma ListT m a
    l = m (Maybe (a, ListT m a)) -> ListT m a
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (m (Maybe (a, ListT m a)) -> ListT m a)
    -> m (Maybe (a, ListT m a)) -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ ((a, ListT m a) -> Maybe (a, ListT m a)
    forall a. a -> Maybe a
    Just ((a, ListT m a) -> Maybe (a, ListT m a))
    -> (a -> (a, ListT m a)) -> a -> Maybe (a, ListT m a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (,ListT m a
    l)) (a -> Maybe (a, ListT m a)) -> m a -> m (Maybe (a, ListT m a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m a
    ma
    -- consMListT ma l = runMListT $ liftM (`consListT` l) ma

    -- simplification:
    -- consMListT ma l = ListT $ runListT =<< liftM (`consListT` l) ma
    -- consMListT ma l = ListT $ runListT =<< (`consListT` l) <$> ma
    -- consMListT ma l = ListT $ runListT =<< do a <- ma; return $ a `consListT` l
    -- consMListT ma l = ListT $ do a <- ma; runListT =<< do return $ a `consListT` l
    -- consMListT ma l = ListT $ do a <- ma; runListT $ a `consListT` l
    -- consMListT ma l = ListT $ do a <- ma; runListT $ ListT $ return $ Just (a, l)
    -- consMListT ma l = ListT $ do a <- ma; return $ Just (a, l)
    -- consMListT ma l = ListT $ Just . (,l) <$> ma

    -- | Monadic singleton.
    sgMListT ::  Monad m => m a -> ListT m a
    sgMListT :: forall (m :: * -> *) a. Monad m => m a -> ListT m a
    sgMListT m a
    ma = m a -> ListT m a -> ListT m a
    forall (m :: * -> *) a. Monad m => m a -> ListT m a -> ListT m a
    consMListT m a
    ma ListT m a
    forall (m :: * -> *) a. Monad m => ListT m a
    nilListT

    -- | Extending a monadic function to 'ListT'.
    mapMListT :: Monad m => (a -> m b) -> ListT m a -> ListT m b
    mapMListT :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ListT m a -> ListT m b
    mapMListT a -> m b
    f (ListT m (Maybe (a, ListT m a))
    ml) = m (Maybe (b, ListT m b)) -> ListT m b
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (m (Maybe (b, ListT m b)) -> ListT m b)
    -> m (Maybe (b, ListT m b)) -> ListT m b
    forall a b. (a -> b) -> a -> b
    $ do
      m (Maybe (a, ListT m a))
    -> m (Maybe (b, ListT m b))
    -> ((a, ListT m a) -> m (Maybe (b, ListT m b)))
    -> m (Maybe (b, ListT m b))
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM m (Maybe (a, ListT m a))
    ml (Maybe (b, ListT m b) -> m (Maybe (b, ListT m b))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (b, ListT m b)
    forall a. Maybe a
    Nothing) (((a, ListT m a) -> m (Maybe (b, ListT m b)))
     -> m (Maybe (b, ListT m b)))
    -> ((a, ListT m a) -> m (Maybe (b, ListT m b)))
    -> m (Maybe (b, ListT m b))
    forall a b. (a -> b) -> a -> b
    $ \ (a
    a, ListT m a
    as) -> do
        b
    b  <- a -> m b
    f a
    a
        Maybe (b, ListT m b) -> m (Maybe (b, ListT m b))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (b, ListT m b) -> m (Maybe (b, ListT m b)))
    -> Maybe (b, ListT m b) -> m (Maybe (b, ListT m b))
    forall a b. (a -> b) -> a -> b
    $ (b, ListT m b) -> Maybe (b, ListT m b)
    forall a. a -> Maybe a
    Just (b
    b , (a -> m b) -> ListT m a -> ListT m b
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ListT m a -> ListT m b
    mapMListT a -> m b
    f ListT m a
    as)

    -- | Alternative implementation using 'foldListT'.
    mapMListT_alt :: Monad m => (a -> m b) -> ListT m a -> ListT m b
    mapMListT_alt :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ListT m a -> ListT m b
    mapMListT_alt a -> m b
    f = m (ListT m b) -> ListT m b
    forall (m :: * -> *) a. Monad m => m (ListT m a) -> ListT m a
    runMListT (m (ListT m b) -> ListT m b)
    -> (ListT m a -> m (ListT m b)) -> ListT m a -> ListT m b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> m (ListT m b) -> m (ListT m b))
    -> m (ListT m b) -> ListT m a -> m (ListT m b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT a -> m (ListT m b) -> m (ListT m b)
    cons (ListT m b -> m (ListT m b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ListT m b
    forall (m :: * -> *) a. Monad m => ListT m a
    nilListT)
      where cons :: a -> m (ListT m b) -> m (ListT m b)
    cons a
    a m (ListT m b)
    ml = m b -> ListT m b -> ListT m b
    forall (m :: * -> *) a. Monad m => m a -> ListT m a -> ListT m a
    consMListT (a -> m b
    f a
    a) (ListT m b -> ListT m b) -> m (ListT m b) -> m (ListT m b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (ListT m b)
    ml

    -- | Change from one monad to another
    liftListT :: (Monad m, Monad m') => (forall a. m a -> m' a) -> ListT m a -> ListT m' a
    liftListT :: forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a. m a -> m' a) -> ListT m a -> ListT m' a
    liftListT forall a. m a -> m' a
    lift ListT m a
    xs = m' (ListT m' a) -> ListT m' a
    forall (m :: * -> *) a. Monad m => m (ListT m a) -> ListT m a
    runMListT (m' (ListT m' a) -> ListT m' a) -> m' (ListT m' a) -> ListT m' a
    forall a b. (a -> b) -> a -> b
    $ m' (Maybe (a, ListT m a))
    -> m' (ListT m' a)
    -> ((a, ListT m a) -> m' (ListT m' a))
    -> m' (ListT m' a)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (m (Maybe (a, ListT m a)) -> m' (Maybe (a, ListT m a))
    forall a. m a -> m' a
    lift (m (Maybe (a, ListT m a)) -> m' (Maybe (a, ListT m a)))
    -> m (Maybe (a, ListT m a)) -> m' (Maybe (a, ListT m a))
    forall a b. (a -> b) -> a -> b
    $ ListT m a -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
    runListT ListT m a
    xs) (ListT m' a -> m' (ListT m' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ListT m' a
    forall (m :: * -> *) a. Monad m => ListT m a
    nilListT) (((a, ListT m a) -> m' (ListT m' a)) -> m' (ListT m' a))
    -> ((a, ListT m a) -> m' (ListT m' a)) -> m' (ListT m' a)
    forall a b. (a -> b) -> a -> b
    $
        \(a
    x,ListT m a
    xs) -> ListT m' a -> m' (ListT m' a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ListT m' a -> m' (ListT m' a)) -> ListT m' a -> m' (ListT m' a)
    forall a b. (a -> b) -> a -> b
    $ a -> ListT m' a -> ListT m' a
    forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
    consListT a
    x (ListT m' a -> ListT m' a) -> ListT m' a -> ListT m' a
    forall a b. (a -> b) -> a -> b
    $ (forall a. m a -> m' a) -> ListT m a -> ListT m' a
    forall (m :: * -> *) (m' :: * -> *) a.
    (Monad m, Monad m') =>
    (forall a. m a -> m' a) -> ListT m a -> ListT m' a
    liftListT forall a. m a -> m' a
    lift ListT m a
    xs

    -- Instances

    instance Monad m => Semigroup (ListT m a) where
      ListT m a
    l1 <> :: ListT m a -> ListT m a -> ListT m a
    <> ListT m a
    l2 = m (Maybe (a, ListT m a)) -> ListT m a
    forall (m :: * -> *) a. m (Maybe (a, ListT m a)) -> ListT m a
    ListT (m (Maybe (a, ListT m a)) -> ListT m a)
    -> m (Maybe (a, ListT m a)) -> ListT m a
    forall a b. (a -> b) -> a -> b
    $ (a -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
    -> m (Maybe (a, ListT m a))
    -> ListT m a
    -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b -> m b) -> m b -> ListT m a -> m b
    foldListT ((ListT m a -> ListT m a)
    -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a (n :: * -> *) b.
    (ListT m a -> ListT n b)
    -> m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b))
    unmapListT ((ListT m a -> ListT m a)
     -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
    -> (a -> ListT m a -> ListT m a)
    -> a
    -> m (Maybe (a, ListT m a))
    -> m (Maybe (a, ListT m a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> ListT m a -> ListT m a
    forall (m :: * -> *) a. Monad m => a -> ListT m a -> ListT m a
    consListT) (ListT m a -> m (Maybe (a, ListT m a))
    forall (m :: * -> *) a. ListT m a -> m (Maybe (a, ListT m a))
    runListT ListT m a
    l2) ListT m a
    l1

    instance Monad m => Monoid (ListT m a) where
      mempty :: ListT m a
    mempty        = ListT m a
    forall (m :: * -> *) a. Monad m => ListT m a
    nilListT
    #if !(MIN_VERSION_base(4,11,0))
      mappend = (<>)
    #endif

    instance (Functor m, Applicative m, Monad m) => Alternative (ListT m) where
      empty :: forall a. ListT m a
    empty = ListT m a
    forall a. Monoid a => a
    mempty
      <|> :: forall a. ListT m a -> ListT m a -> ListT m a
    (<|>) = ListT m a -> ListT m a -> ListT m a
    forall a. Monoid a => a -> a -> a
    mappend

    instance (Functor m, Applicative m, Monad m) => MonadPlus (ListT m) where
      mzero :: forall a. ListT m a
    mzero = ListT m a
    forall a. Monoid a => a
    mempty
      mplus :: forall a. ListT m a -> ListT m a -> ListT m a
    mplus = ListT m a -> ListT m a -> ListT m a
    forall a. Monoid a => a -> a -> a
    mappend

    instance (Functor m, Applicative m, Monad m) => Applicative (ListT m) where
      pure :: forall a. a -> ListT m a
    pure  = a -> ListT m a
    forall (m :: * -> *) a. Monad m => a -> ListT m a
    sgListT
      <*> :: forall a b. ListT m (a -> b) -> ListT m a -> ListT m b
    (<*>) = ListT m (a -> b) -> ListT m a -> ListT m b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

      -- Another Applicative, but not the canonical one.
      -- l1 <*> l2 = ListT $ loop <$> runListT l1 <*> runListT l2
      --   where
      --   loop (Just (f, l1')) (Just (a, l2')) = Just (f a, l1' <*> l2')
      --   loop _ _ = Nothing

    instance (Functor m, Applicative m, Monad m) => Monad (ListT m) where
      return :: forall a. a -> ListT m a
    return  = a -> ListT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      ListT m a
    l >>= :: forall a b. ListT m a -> (a -> ListT m b) -> ListT m b
    >>= a -> ListT m b
    k = ListT m (ListT m b) -> ListT m b
    forall (m :: * -> *) a. Monad m => ListT m (ListT m a) -> ListT m a
    concatListT (ListT m (ListT m b) -> ListT m b)
    -> ListT m (ListT m b) -> ListT m b
    forall a b. (a -> b) -> a -> b
    $ a -> ListT m b
    k (a -> ListT m b) -> ListT m a -> ListT m (ListT m b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ListT m a
    l

    instance MonadTrans ListT where
      lift :: forall (m :: * -> *) a. Monad m => m a -> ListT m a
    lift = m a -> ListT m a
    forall (m :: * -> *) a. Monad m => m a -> ListT m a
    sgMListT

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

    instance (Applicative m, MonadReader r m) => MonadReader r (ListT m) where
      ask :: ListT m r
    ask     = m r -> ListT m r
    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) -> ListT m a -> ListT m a
    local   = (m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
    -> ListT m a -> ListT m a
    forall (m :: * -> *) a (n :: * -> *) b.
    (m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
    -> ListT m a -> ListT n b
    mapListT ((m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
     -> ListT m a -> ListT m a)
    -> ((r -> r)
        -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a)))
    -> (r -> r)
    -> ListT m a
    -> ListT m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (r -> r) -> m (Maybe (a, ListT m a)) -> m (Maybe (a, ListT m a))
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local

    instance (Applicative m, MonadState s m) => MonadState s (ListT m) where
      get :: ListT m s
    get = m s -> ListT m s
    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 -> ListT m ()
    put = m () -> ListT m ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m () -> ListT m ()) -> (s -> m ()) -> s -> ListT m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . s -> m ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put

    instance Monad m => MonadFail (ListT m) where
      fail :: forall a. String -> ListT m a
    fail String
    _ = ListT m a
    forall (f :: * -> *) a. Alternative f => f a
    empty