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 |
|
ImpMissingDefinitions [String] String | We reached a program point without all the required
primitives or BUILTIN to proceed forward.
|
Instances
Show Impossible Source # | |
Defined in Agda.Utils.Impossible Methods showsPrec :: Int -> Impossible -> ShowS show :: Impossible -> String showList :: [Impossible] -> ShowS | |
Exception Impossible Source # | |
Defined in Agda.Utils.Impossible Methods toException :: Impossible -> SomeException fromException :: SomeException -> Maybe Impossible displayException :: Impossible -> String | |
EmbPrj Impossible Source # | |
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.