ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.Impossible

An interface for reporting "impossible" errors

1 type
1 class
4 values

PackageAgda-2.7.0.1
Exports6
LanguageHaskell2010
LicenceMIT
SourceImpossible.hs

datadata 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

Instances6Eq, Ord, Show, Exception, NFData, EmbPrj

Eq ImpossibleDefined in Agda-2.7.0.1 · Agda.Utils.Impossible
Ord ImpossibleDefined in Agda-2.7.0.1 · Agda.Utils.Impossible
Show ImpossibleDefined in Agda-2.7.0.1 · Agda.Utils.Impossible
Exception ImpossibleDefined in Agda-2.7.0.1 · Agda.Utils.Impossible
NFData ImpossibleDefined in Agda-2.7.0.1 · Agda.Utils.Impossible
EmbPrj ImpossibleDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Common · orphan

valuethrowImpossible :: Impossible -> a

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

classclass CatchImpossible (m :: Type -> Type) where

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

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.

Instances2CatchImpossible

CatchImpossible TCMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
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.
CatchImpossible IODefined in Agda-2.7.0.1 · Agda.Utils.Impossible

value__IMPOSSIBLE__ :: HasCallStack => a

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

valueimpossible :: HasCallStack => Impossible

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