    -- | Non-empty maps.
    --
    --   Provides type @Map1@ of non-empty maps.
    --
    --   Import:
    --   @
    --
    --     import           Agda.Utils.Map1 (Map1)
    --     import qualified Agda.Utils.Map1 as Map1
    --
    --   @

    module Agda.Utils.Map1
      ( module Agda.Utils.Map1
      , module Map1
      ) where

    import Data.Map (Map)
    import Data.Map.NonEmpty as Map1

    type Map1 = Map1.NEMap

    ifNull :: Map k a -> b -> (Map1 k a -> b) -> b
    ifNull :: forall k a b. Map k a -> b -> (Map1 k a -> b) -> b
    ifNull Map k a
    s b
    b Map1 k a -> b
    f = b -> (Map1 k a -> b) -> Map k a -> b
    forall r k a. r -> (NEMap k a -> r) -> Map k a -> r
    Map1.withNonEmpty b
    b Map1 k a -> b
    f Map k a
    s

    -- | A more general type would be @Null m => Map k a -> (Map1 k a -> m) -> m@
    --   but this type is problematic as we do not have a general
    --   @instance Applicative m => Null (m ())@.
    --
    unlessNull :: Applicative m => Map k a -> (Map1 k a -> m ()) -> m ()
    unlessNull :: forall (m :: * -> *) k a.
    Applicative m =>
    Map k a -> (Map1 k a -> m ()) -> m ()
    unlessNull = ((Map1 k a -> m ()) -> Map k a -> m ())
    -> Map k a -> (Map1 k a -> m ()) -> m ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (((Map1 k a -> m ()) -> Map k a -> m ())
     -> Map k a -> (Map1 k a -> m ()) -> m ())
    -> ((Map1 k a -> m ()) -> Map k a -> m ())
    -> Map k a
    -> (Map1 k a -> m ())
    -> m ()
    forall a b. (a -> b) -> a -> b
    $ m () -> (Map1 k a -> m ()) -> Map k a -> m ()
    forall r k a. r -> (NEMap k a -> r) -> Map k a -> r
    Map1.withNonEmpty (m () -> (Map1 k a -> m ()) -> Map k a -> m ())
    -> m () -> (Map1 k a -> m ()) -> Map k a -> m ()
    forall a b. (a -> b) -> a -> b
    $ () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
    {-# INLINE unlessNull #-}

    unlessNullM :: Monad m => m (Map k a) -> (Map1 k a -> m ()) -> m ()
    unlessNullM :: forall (m :: * -> *) k a.
    Monad m =>
    m (Map k a) -> (Map1 k a -> m ()) -> m ()
    unlessNullM m (Map k a)
    m Map1 k a -> m ()
    k = m (Map k a)
    m m (Map k a) -> (Map k a -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (Map k a -> (Map1 k a -> m ()) -> m ()
    forall (m :: * -> *) k a.
    Applicative m =>
    Map k a -> (Map1 k a -> m ()) -> m ()
    `unlessNull` Map1 k a -> m ()
    k)
    {-# INLINE unlessNullM #-}