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

Safe Haskell | Safe
Language | Haskell2010

Agda.Utils.Impossible

Description

An interface for reporting "impossible" errors

Synopsis

- data Impossible
  - = Impossible String Integer
  - | Unreachable String Integer
  - | ImpMissingDefinitions [String] String
- throwImpossible :: Impossible -> a
- catchImpossible :: IO a -> (Impossible -> IO a) -> IO 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 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 Source # |
Instance details Defined in Agda.Utils.Impossible Methods showsPrec :: Int -> Impossible -> ShowS Source # show :: Impossible -> String Source # showList :: [Impossible] -> ShowS Source #
Exception Impossible Source # |
Instance details Defined in Agda.Utils.Impossible Methods toException :: Impossible -> SomeException Source # fromException :: SomeException -> Maybe Impossible Source # displayException :: Impossible -> String Source #
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 the macro in `undefined.h`.

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

Catch an "impossible" error, if possible.