{-# OPTIONS_GHC -Wunused-imports #-}

-- | An empty type with some useful instances.
module Mikan.Utils.Empty
  ( Empty
  , absurd
  , toImpossible
  )
  where

import Control.DeepSeq
import Control.Exception (evaluate)

import Mikan.Utils.Impossible

-- | A type with no inhabitants.
--
-- Note that 'Empty' and 'Data.Void.Void' are NOT interchangable,
-- as they have different 'NFData' instances. In particular,
-- the 'NFData' instance for 'Data.Void.Void' forces the value. This
-- is typically not desirable, as we often want to use 'Empty' as a proxy
-- for an '__IMPOSSIBLE__'.
data Empty

-- | Values of type 'Empty' are not forced.
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 \"Mikan.Utils.Empty.Empty\""

-- | Force an 'Empty'.
absurd :: Empty -> a
absurd :: forall a. Empty -> a
absurd Empty
e = Empty -> a -> a
forall a b. a -> b -> b
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
  s <- IO (Maybe Impossible)
-> (Impossible -> IO (Maybe Impossible)) -> IO (Maybe Impossible)
forall a. IO a -> (Impossible -> IO a) -> IO a
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 a b. a -> IO b -> IO a
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 a. a -> IO a
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 s of
    Just Impossible
i  -> Impossible -> IO Impossible
forall a. a -> IO a
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