    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An effectful view of List
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.List.NonEmpty.Effectful.Transformer where

    open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_)
    open import Effect.Functor using (RawFunctor)
    open import Effect.Applicative using (RawApplicative)
    open import Effect.Monad using (RawMonad; RawMonadT)
    open import Function.Base using (_∘′_; _∘_; _$_)
    open import Level using (Level)

    import Data.List.NonEmpty.Effectful as List⁺ using (module TraversableM)

    private
      variable
        f g : Level
        M : Set f → Set g

    ------------------------------------------------------------------------
    -- List⁺ monad transformer

    record List⁺T (M : Set f → Set g) (A : Set f) : Set g where
      constructor mkList⁺T
      field runList⁺T : M (List⁺ A)
    open List⁺T public

    functor : RawFunctor M → RawFunctor {f} (List⁺T M)
    functor M = record
      { _<$>_ = λ f → mkList⁺T ∘′ (List⁺.map f <$>_) ∘′ runList⁺T
      } where open RawFunctor M

    applicative : RawApplicative M → RawApplicative {f} (List⁺T M)
    applicative M = record
      { rawFunctor = functor rawFunctor
      ; pure = mkList⁺T ∘′ pure ∘′ List⁺.[_]
      ; _<*>_  = λ mf ma → mkList⁺T (List⁺.ap <$> runList⁺T mf <*> runList⁺T ma)
      } where open RawApplicative M

    monad : RawMonad M → RawMonad (List⁺T M)
    monad M = record
      { rawApplicative = applicative rawApplicative
      ; _>>=_ = λ mas f → mkList⁺T $ do
                           as ← runList⁺T mas
                           List⁺.concat <$> mapM (runList⁺T ∘′ f) as
      } where open RawMonad M; open List⁺.TraversableM M

    monadT : RawMonadT {f} {g} List⁺T
    monadT M = record
      { lift = mkList⁺T ∘′ (List⁺.[_] <$>_)
      ; rawMonad = monad M
      } where open RawMonad M