content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  -- | An empty type with some useful instances.
  module Agda.Utils.Empty where
  
  import Control.DeepSeq
  import Control.Exception (evaluate)
  
  import Agda.Utils.Impossible
  
  
  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 _ = ()
  
  instance Eq Empty where
    _ == _ = True
  
  instance Ord Empty where
    compare _ _ = EQ
  
  instance Show Empty where
    showsPrec p _ = showParen (p > 9) $ showString "error \"Agda.Utils.Empty.Empty\""
  
  absurd :: Empty -> a
  absurd e = seq e __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 e = do
    s <- catchImpossible (Nothing <$ evaluate e) (return . Just)
    case s of
      Just i  -> return i
      Nothing -> absurd e -- this should never happen
  