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. MissingDefinitions needed 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 the macro in undefined.h.

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

Catch an "impossible" error, if possible.