Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.Impossible

Description

An interface for reporting "impossible" errors

Synopsis

Documentation

data Impossible Source #

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

Constructors

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

Instances

Instances details
EmbPrj Impossible Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Impossible -> S Int32 Source #

icod_ :: Impossible -> S Int32 Source #

value :: Int32 -> R Impossible Source #

Exception Impossible Source # 
Instance details

Defined in Agda.Utils.Impossible

Methods

toException :: Impossible -> SomeException

fromException :: SomeException -> Maybe Impossible

displayException :: Impossible -> String

Show Impossible Source # 
Instance details

Defined in Agda.Utils.Impossible

Methods

showsPrec :: Int -> Impossible -> ShowS

show :: Impossible -> String

showList :: [Impossible] -> ShowS

NFData Impossible Source # 
Instance details

Defined in Agda.Utils.Impossible

Methods

rnf :: Impossible -> ()

Eq Impossible Source # 
Instance details

Defined in Agda.Utils.Impossible

Methods

(==) :: Impossible -> Impossible -> Bool

(/=) :: Impossible -> Impossible -> Bool

Ord Impossible Source # 
Instance details

Defined in Agda.Utils.Impossible

throwImpossible :: Impossible -> a Source #

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

class CatchImpossible m where Source #

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 Source #

Catch any Impossible exception.

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

Catch only Impossible exceptions selected by the filter.

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

Version of catchImpossible with argument order suiting short handlers.

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

Version of catchImpossibleJust with argument order suiting short handlers.

Instances

Instances details
CatchImpossible TCM Source #

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.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

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

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

CatchImpossible IO Source # 
Instance details

Defined in Agda.Utils.Impossible

Methods

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

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

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

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

__IMPOSSIBLE__ :: HasCallStack => a Source #

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

__UNREACHABLE__ :: HasCallStack => a Source #

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.