Safe Haskell	None
Language	Haskell2010

Agda.Utils.Impossible

Description

An interface for reporting "impossible" errors

Synopsis

data Impossible
- = Impossible CallStack
- | Unreachable CallStack
- | ImpMissingDefinitions [String] String
throwImpossible :: Impossible -> a
class CatchImpossible m where
- catchImpossible :: m a -> (Impossible -> m a) -> m a
- catchImpossibleJust :: (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
- handleImpossible :: (Impossible -> m a) -> m a -> m a
- handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> m a) -> m a -> m a
__IMPOSSIBLE__ :: HasCallStack => a
impossible :: HasCallStack => Impossible
__UNREACHABLE__ :: HasCallStack => a

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

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 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 #
Show Impossible Source #
Instance details Defined in Agda.Utils.Impossible Methods showsPrec :: Int -> Impossible -> ShowS # show :: Impossible -> String # showList :: [Impossible] -> ShowS #
Exception Impossible Source #
Instance details Defined in Agda.Utils.Impossible Methods toException :: Impossible -> SomeException # fromException :: SomeException -> Maybe Impossible # displayException :: Impossible -> String #
NFData Impossible Source #
Instance details Defined in Agda.Utils.Impossible Methods rnf :: Impossible -> () #
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 #

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

__IMPOSSIBLE__ :: HasCallStack => a Source #

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

impossible :: HasCallStack => Impossible Source #

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