    -- | Facility to test throwing internal errors.

    module Agda.ImpossibleTest where

    import Agda.TypeChecking.Monad.Base   ( TCM, ReduceM, runReduceM )
    import Agda.TypeChecking.Monad.Debug  ( MonadDebug, __IMPOSSIBLE_VERBOSE__ )
    import Agda.TypeChecking.Reduce.Monad ()

    import Agda.Utils.CallStack           ( HasCallStack )
    import Agda.Utils.Impossible          ( __IMPOSSIBLE__ )

    -- | If the given list of words is non-empty, print them as debug message
    --   (using '__IMPOSSIBLE_VERBOSE__') before raising the internal error.
    impossibleTest :: (MonadDebug m, HasCallStack) => [String] -> m a
    impossibleTest :: forall (m :: * -> *) a.
    (MonadDebug m, HasCallStack) =>
    [String] -> m a
    impossibleTest = \case
      []   -> m a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      [String]
    strs -> String -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ (String -> m a) -> String -> m a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String]
    strs

    impossibleTestReduceM :: (HasCallStack) => [String] -> TCM a
    impossibleTestReduceM :: forall a. HasCallStack => [String] -> TCM a
    impossibleTestReduceM = ReduceM a -> TCM a
    forall a. ReduceM a -> TCM a
    runReduceM (ReduceM a -> TCM a)
    -> ([String] -> ReduceM a) -> [String] -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . \case
      []   -> ReduceM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      [String]
    strs -> String -> ReduceM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ (String -> ReduceM a) -> String -> ReduceM a
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [String]
    strs