{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Utils.Empty where
import Control.Exception (evaluate)
import Data.Functor ((<$))
import Data.Data (Data)
import Agda.Utils.Impossible
#include "undefined.h"
data Empty
deriving instance Data Empty
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 :: Empty -> IO Impossible
toImpossible e = do
s <- catchImpossible (Nothing <$ evaluate e) (return . Just)
case s of
Just i -> return i
Nothing -> absurd e