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