    -- | An empty type with some useful instances.
    module Agda.Utils.Empty where

    import Control.DeepSeq
    import Control.Exception (evaluate)

    import Data.Data (Data)

    import Agda.Utils.Impossible

    data Empty

    deriving instance Data Empty

    -- | Values of type 'Empty' are not forced, because 'Empty' is used as
    -- a constructor argument in 'Agda.Syntax.Internal.Substitution''.

    instance NFData Empty where
      rnf :: Empty -> ()
    rnf Empty
    _ = ()

    instance Eq Empty where
      Empty
    _ == :: Empty -> Empty -> Bool
    == Empty
    _ = Bool
    True

    instance Ord Empty where
      compare :: Empty -> Empty -> Ordering
    compare Empty
    _ Empty
    _ = Ordering
    EQ

    instance Show Empty where
      showsPrec :: Int -> Empty -> ShowS
    showsPrec Int
    p Empty
    _ = Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    9) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ String -> ShowS
    showString String
    "error \"Agda.Utils.Empty.Empty\""

    absurd :: Empty -> a
    absurd :: forall a. Empty -> a
    absurd Empty
    e = Empty -> a -> a
    seq Empty
    e a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | @toImpossible e@ extracts the @Impossible@ value raised via
    --   @__IMPOSSIBLE__@ to create the element @e@ of type @Empty@.
    --   It proceeds by evaluating @e@ to weak head normal form and
    --   catching the exception.
    --   We are forced to wrap things in a @Maybe@ because of
    --   @catchImpossible@'s type.

    toImpossible :: Empty -> IO Impossible
    toImpossible :: Empty -> IO Impossible
    toImpossible Empty
    e = do
      Maybe Impossible
    s <- IO (Maybe Impossible)
    -> (Impossible -> IO (Maybe Impossible)) -> IO (Maybe Impossible)
    forall (m :: * -> *) a.
    CatchImpossible m =>
    m a -> (Impossible -> m a) -> m a
    catchImpossible (Maybe Impossible
    forall a. Maybe a
    Nothing Maybe Impossible -> IO Empty -> IO (Maybe Impossible)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Empty -> IO Empty
    forall a. a -> IO a
    evaluate Empty
    e) (Maybe Impossible -> IO (Maybe Impossible)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Impossible -> IO (Maybe Impossible))
    -> (Impossible -> Maybe Impossible)
    -> Impossible
    -> IO (Maybe Impossible)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Impossible -> Maybe Impossible
    forall a. a -> Maybe a
    Just)
      case Maybe Impossible
    s of
        Just Impossible
    i  -> Impossible -> IO Impossible
    forall (m :: * -> *) a. Monad m => a -> m a
    return Impossible
    i
        Maybe Impossible
    Nothing -> Empty -> IO Impossible
    forall a. Empty -> a
    absurd Empty
    e -- this should never happen