Agda-2.6.0: A dependently typed functional programming language and proof assistant

Safe HaskellSafe



An interface for reporting "impossible" errors



data Impossible Source #

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


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. MissingDefinitions needed forthis

throwImpossible :: Impossible -> a Source #

Abort by throwing an "impossible" error. You should not use this function directly. Instead use the macro in undefined.h.

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

Catch an "impossible" error, if possible.