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

EmbPrj Impossible

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Impossible -> S Int32

icod_ :: Impossible -> S Int32

value :: Int32 -> R Impossible

Exception Impossible

Defined in Agda.Utils.Impossible

Methods

toException :: Impossible -> SomeException

fromException :: SomeException -> Maybe Impossible

displayException :: Impossible -> String

Show Impossible

Defined in Agda.Utils.Impossible

Methods

showsPrec :: Int -> Impossible -> ShowS

show :: Impossible -> String

showList :: [Impossible] -> ShowS

NFData Impossible

Defined in Agda.Utils.Impossible

Methods

rnf :: Impossible -> ()

Eq Impossible

Defined in Agda.Utils.Impossible

Methods

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

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

Ord Impossible

Defined in Agda.Utils.Impossible

Methods

compare :: Impossible -> Impossible -> Ordering

(<) :: Impossible -> Impossible -> Bool

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

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

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

max :: Impossible -> Impossible -> Impossible

min :: Impossible -> Impossible -> Impossible

throwImpossible :: Impossible -> a

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

class CatchImpossible (m :: Type -> Type) 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 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

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

__IMPOSSIBLE__ :: HasCallStack => a

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

impossible :: HasCallStack => Impossible

__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.