Agda.Utils.Impossible

An interface for reporting "impossible" errors

Documentation

data Impossible

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

Constructors

Impossible String Integer

We reached a program point which should be unreachable.

Unreachable String Integer

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

Instances

Show Impossible

Defined in Agda.Utils.Impossible

Methods

showsPrec :: Int -> Impossible -> ShowS

show :: Impossible -> String

showList :: [Impossible] -> ShowS

Exception Impossible

Defined in Agda.Utils.Impossible

Methods

toException :: Impossible -> SomeException

fromException :: SomeException -> Maybe Impossible

displayException :: Impossible -> String

EmbPrj Impossible

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Impossible -> S Int32

icod_ :: Impossible -> S Int32

value :: Int32 -> R Impossible

throwImpossible :: Impossible -> a

Abort by throwing an "impossible" error. You should not use this function directly. Instead use IMPOSSIBLE

class CatchImpossible m where

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

Minimal complete definition

catchImpossibleJust | handleImpossibleJust

Methods

catchImpossible :: m a -> (Impossible -> m a) -> m a

Catch any Impossible exception.

catchImpossibleJust :: (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a

Catch only Impossible exceptions selected by the filter.

handleImpossible :: (Impossible -> m a) -> m a -> m a

Version of catchImpossible with argument order suiting short handlers.

handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a

Version of catchImpossibleJust with argument order suiting short handlers.

Instances

CatchImpossible IO

Defined in Agda.Utils.Impossible

Methods

catchImpossible :: IO a -> (Impossible -> IO a) -> IO a

catchImpossibleJust :: (Impossible -> Maybe b) -> IO a -> (b -> IO a) -> IO a

handleImpossible :: (Impossible -> IO a) -> IO a -> IO a

handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> IO a) -> IO a -> IO a

CatchImpossible TCM

Like catchError, but resets the state completely before running the handler. This means it also loses changes to the stPersistentState.

The intended use is to catch internal errors during debug printing. In debug printing, we are not expecting state changes.

Defined in Agda.TypeChecking.Monad.Base

Methods

catchImpossible :: TCM a -> (Impossible -> TCM a) -> TCM a

catchImpossibleJust :: (Impossible -> Maybe b) -> TCM a -> (b -> TCM a) -> TCM a

handleImpossible :: (Impossible -> TCM a) -> TCM a -> TCM a

handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> TCM a) -> TCM a -> TCM a

withFileAndLine' :: Integral a => CallStack -> (String -> a -> b) -> b

Create something with a callstack's file and line number

withFileAndLine :: (HasCallStack, Integral a) => (String -> a -> b) -> b

Create something with the call site's file and line number

__IMPOSSIBLE__ :: HasCallStack => a

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

__UNREACHABLE__ :: HasCallStack => a

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.