    {-# LANGUAGE CPP #-}

    {-# OPTIONS_GHC -Wunused-imports #-}

    ------------------------------------------------------------------------
    -- | An interface for reporting \"impossible\" errors
    ------------------------------------------------------------------------

    module Agda.Utils.Impossible where

    import Control.Exception (Exception(..), throw, catchJust)
    import Control.DeepSeq
    import Agda.Utils.CallStack.Base
        ( CallStack
        , HasCallStack
        , prettyCallStack
        , withCallerCallStack
        , withNBackCallStack
        )

    -- | \"Impossible\" errors, annotated with a file name and a line
    -- number corresponding to the source code location of the error.

    data Impossible

      = Impossible CallStack
        -- ^ We reached a program point which should be unreachable.

      | Unreachable CallStack
        -- ^ @Impossible@ with a different error message.
        --   Used when we reach a program point which can in principle
        --   be reached, but not for a certain run.

      | ImpMissingDefinitions [String] String
        -- ^ We reached a program point without all the required
        -- primitives or BUILTIN to proceed forward.
        -- @ImpMissingDefinitions neededDefs forThis@

    -- Identify all values of Impossible. We use Impossible as a stand-in for the empty type, so all
    -- values are morally equal.
    instance Eq Impossible where
      Impossible
    _ == :: Impossible -> Impossible -> Bool
    == Impossible
    _ = Bool
    True

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

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

    instance Show Impossible where
      show :: Impossible -> String
    show (Impossible CallStack
    loc) = [String] -> String
    unlines
        [ String
    "An internal error has occurred. Please report this as a bug."
        , String
    "Location of the error: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ CallStack -> String
    prettyCallStack CallStack
    loc
        ]
      show (Unreachable CallStack
    loc) = [String] -> String
    unlines
        [ String
    "We reached a program point we did not want to reach."
        , String
    "Location of the error: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ CallStack -> String
    prettyCallStack CallStack
    loc
        ]
      show (ImpMissingDefinitions [String]
    needed String
    forthis) = [String] -> String
    unlines
        [ String
    "The following builtins or primitives need to be bound to use " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    forthis String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ":"
        , [String] -> String
    unwords [String]
    needed
        ]

    instance Exception Impossible where
    #if MIN_VERSION_base(4,20,0)
      -- Andreas, 2024-07-05, issue #7299;
      -- Turn off the (here useless) backtrace introduced in GHC 9.10.
      -- Besides spamming us with useless info, it changes the golden
      -- value, introducing incompatibilities in the test-suite.
      backtraceDesired :: Impossible -> Bool
    backtraceDesired Impossible
    _ = Bool
    False
    #endif

    -- | Abort by throwing an \"impossible\" error. You should not use
    -- this function directly. Instead use __IMPOSSIBLE__

    throwImpossible :: Impossible -> a
    throwImpossible :: forall a. Impossible -> a
    throwImpossible = Impossible -> a
    forall a e. (HasCallStack, Exception e) => e -> a
    throw

    -- | Monads in which we can catch an \"impossible\" error, if possible.

    class CatchImpossible m where

      -- | Catch any 'Impossible' exception.
      catchImpossible :: m a -> (Impossible -> m a) -> m a
      catchImpossible = (Impossible -> Maybe Impossible)
    -> m a -> (Impossible -> m a) -> m a
    forall b a. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
    forall (m :: * -> *) b a.
    CatchImpossible m =>
    (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
    catchImpossibleJust Impossible -> Maybe Impossible
    forall a. a -> Maybe a
    Just

      -- | Catch only 'Impossible' exceptions selected by the filter.
      catchImpossibleJust :: (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
      catchImpossibleJust = ((b -> m a) -> m a -> m a) -> m a -> (b -> m a) -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (((b -> m a) -> m a -> m a) -> m a -> (b -> m a) -> m a)
    -> ((Impossible -> Maybe b) -> (b -> m a) -> m a -> m a)
    -> (Impossible -> Maybe b)
    -> m a
    -> (b -> m a)
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
    forall b a. (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
    forall (m :: * -> *) b a.
    CatchImpossible m =>
    (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
    handleImpossibleJust

      -- | Version of 'catchImpossible' with argument order suiting short handlers.
      handleImpossible :: (Impossible -> m a) -> m a -> m a
      handleImpossible = (m a -> (Impossible -> m a) -> m a)
    -> (Impossible -> m a) -> m a -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip m a -> (Impossible -> m a) -> m a
    forall a. m a -> (Impossible -> m a) -> m a
    forall (m :: * -> *) a.
    CatchImpossible m =>
    m a -> (Impossible -> m a) -> m a
    catchImpossible

      -- | Version of 'catchImpossibleJust' with argument order suiting short handlers.
      handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
      handleImpossibleJust = (m a -> (b -> m a) -> m a) -> (b -> m a) -> m a -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((m a -> (b -> m a) -> m a) -> (b -> m a) -> m a -> m a)
    -> ((Impossible -> Maybe b) -> m a -> (b -> m a) -> m a)
    -> (Impossible -> Maybe b)
    -> (b -> m a)
    -> m a
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
    forall b a. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
    forall (m :: * -> *) b a.
    CatchImpossible m =>
    (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
    catchImpossibleJust

      {-# MINIMAL catchImpossibleJust | handleImpossibleJust #-}

    instance CatchImpossible IO where
      catchImpossibleJust :: forall b a. (Impossible -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    catchImpossibleJust = (Impossible -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    catchJust

    -- | Construct a value of 'Impossible' reporting the location where you call
    --   this function.
    impossible :: HasCallStack => Impossible
    impossible :: HasCallStack => Impossible
    impossible = (CallStack -> Impossible) -> Impossible
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> Impossible
    Impossible

    -- | Throw an 'Impossible' error reporting the location where you
    --   place '__IMPOSSIBLE__'.

    __IMPOSSIBLE__ :: HasCallStack => a
    __IMPOSSIBLE__ :: forall a. HasCallStack => a
    __IMPOSSIBLE__ = Word -> (CallStack -> a) -> a
    forall b. HasCallStack => Word -> (CallStack -> b) -> b
    withNBackCallStack Word
    0 ((CallStack -> a) -> a) -> (CallStack -> a) -> a
    forall a b. (a -> b) -> a -> b
    $ Impossible -> a
    forall a. Impossible -> a
    throwImpossible (Impossible -> a) -> (CallStack -> Impossible) -> CallStack -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> Impossible
    Impossible

    -- | Throw an 'Impossible' error reporting the *caller's* call site.

    __IMPOSSIBLE__1 :: HasCallStack => a
    __IMPOSSIBLE__1 :: forall a. HasCallStack => a
    __IMPOSSIBLE__1 = Word -> (CallStack -> a) -> a
    forall b. HasCallStack => Word -> (CallStack -> b) -> b
    withNBackCallStack Word
    1 ((CallStack -> a) -> a) -> (CallStack -> a) -> a
    forall a b. (a -> b) -> a -> b
    $ Impossible -> a
    forall a. Impossible -> a
    throwImpossible (Impossible -> a) -> (CallStack -> Impossible) -> CallStack -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> Impossible
    Impossible

    -- | Throw an "Unreachable" error reporting the *caller's* call site.
    -- Note that this call to "withFileAndLine" will be filtered out
    -- due its filter on the srcLocModule.

    __UNREACHABLE__ :: HasCallStack => a
    __UNREACHABLE__ :: forall a. HasCallStack => a
    __UNREACHABLE__ = (CallStack -> a) -> a
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack ((CallStack -> a) -> a) -> (CallStack -> a) -> a
    forall a b. (a -> b) -> a -> b
    $ Impossible -> a
    forall a. Impossible -> a
    throwImpossible (Impossible -> a) -> (CallStack -> Impossible) -> CallStack -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> Impossible
    Unreachable