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

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

    import Data.Set (Set, empty)
    import Data.Set.NonEmpty as Set1

    type Set1 = Set1.NESet

    ifNull :: Set a -> b -> (Set1 a -> b) -> b
    ifNull :: forall a b. Set a -> b -> (Set1 a -> b) -> b
    ifNull Set a
    s b
    b Set1 a -> b
    f = b -> (Set1 a -> b) -> Set a -> b
    forall r a. r -> (NESet a -> r) -> Set a -> r
    Set1.withNonEmpty b
    b Set1 a -> b
    f Set a
    s

    -- | Lossless 'toSet'.  Opposite of 'nonEmptySet'.

    toSet' :: Maybe (Set1 a) -> Set a
    toSet' :: forall a. Maybe (Set1 a) -> Set a
    toSet' = Set a -> (Set1 a -> Set a) -> Maybe (Set1 a) -> Set a
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Set a
    forall a. Set a
    empty Set1 a -> Set a
    forall a. NESet a -> Set a
    toSet

    -- | A more general type would be @Null m => Set a -> (Set1 a -> m) -> m@
    --   but this type is problematic as we do not have a general
    --   @instance Applicative m => Null (m ())@.
    --
    unlessNull :: Applicative m => Set a -> (Set1 a -> m ()) -> m ()
    unlessNull :: forall (m :: * -> *) a.
    Applicative m =>
    Set a -> (Set1 a -> m ()) -> m ()
    unlessNull = ((Set1 a -> m ()) -> Set a -> m ())
    -> Set a -> (Set1 a -> m ()) -> m ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (((Set1 a -> m ()) -> Set a -> m ())
     -> Set a -> (Set1 a -> m ()) -> m ())
    -> ((Set1 a -> m ()) -> Set a -> m ())
    -> Set a
    -> (Set1 a -> m ())
    -> m ()
    forall a b. (a -> b) -> a -> b
    $ m () -> (Set1 a -> m ()) -> Set a -> m ()
    forall r a. r -> (NESet a -> r) -> Set a -> r
    Set1.withNonEmpty (m () -> (Set1 a -> m ()) -> Set a -> m ())
    -> m () -> (Set1 a -> m ()) -> Set 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 (Set a) -> (Set1 a -> m ()) -> m ()
    unlessNullM :: forall (m :: * -> *) a.
    Monad m =>
    m (Set a) -> (Set1 a -> m ()) -> m ()
    unlessNullM m (Set a)
    m Set1 a -> m ()
    k = m (Set a)
    m m (Set a) -> (Set 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
    >>= (Set a -> (Set1 a -> m ()) -> m ()
    forall (m :: * -> *) a.
    Applicative m =>
    Set a -> (Set1 a -> m ()) -> m ()
    `unlessNull` Set1 a -> m ()
    k)
    {-# INLINE unlessNullM #-}