Safe Haskell	None
Language	Haskell2010

Language.PTS.Error

Description

Errors. Not re-exported by Language.PTS.

Synopsis

Documentation

class Monad m => MonadErr m where Source #

A MonadError Err.

Minimal complete definition

Methods

Instances

MonadErr Maybe Source #
Instance details Defined in Language.PTS.Error Methods throwErr :: Err -> Maybe a Source #
MonadErr IO Source #	Throws `Err` with `throwIO`.
Instance details Defined in Language.PTS.Error Methods throwErr :: Err -> IO a Source #
AsErr err => MonadErr (Either err) Source #
Instance details Defined in Language.PTS.Error Methods throwErr :: Err -> Either err a Source #
(AsErr err, Monad m) => MonadErr (EitherKT err m) Source #
Instance details Defined in Language.PTS.Error Methods throwErr :: Err -> EitherKT err m a Source #
Monad m => MonadErr (ScriptT s m) Source #
Instance details Defined in Language.PTS.Script Methods throwErr :: Err -> ScriptT s m a Source #

Various errors occuring during type-checking of terms.

Constructors

SomeErr String	untyped error. Avoid.
VariableNotInScope (PrettyM Doc) [PrettyM Doc]	variable not in the context provided
TypeMismatch (PrettyM Doc) (PrettyM Doc) (PrettyM Doc) [PrettyM Doc]	type mismatch in function application
NonEqual (PrettyM Doc) (PrettyM Doc) (PrettyM Doc) [PrettyM Doc]	Refl annotated with mismatching values
SortMismatch (PrettyM Doc) (PrettyM Doc) (PrettyM Doc) [PrettyM Doc]	type mismatch in function application
LambdaNotPi (PrettyM Doc) (PrettyM Doc) [PrettyM Doc]	Lambda is (annotated with) not a Pi-type
PairNotSigma (PrettyM Doc) (PrettyM Doc) [PrettyM Doc]	Pair is (annotated with) not a Sigma-type
ReflNotEquality (PrettyM Doc) [PrettyM Doc]	Refl is (annotated with) not an Equality-type
NotAPair (PrettyM Doc) (PrettyM Doc) [PrettyM Doc]	Match on not a pair
NoRule (PrettyM Doc) (PrettyM Doc) [PrettyM Doc]	invalid function space
NotAFunction (PrettyM Doc) (PrettyM Doc) (PrettyM Doc) [PrettyM Doc]	apply warning in `Term` type-checker.
SortWithoutAxiom (PrettyM Doc) [PrettyM Doc]	abstracting over a sort without an axiom.
QuarkNotInHadron Sym (Set Sym) [PrettyM Doc]	quark not in hardon
QuarkNotHadron Sym (PrettyM Doc) [PrettyM Doc]	quark is (annoted with) not a hadron
ApplyPanic String (PrettyM Doc)	apply panic in `Value` evaluator
OccursFailure (PrettyM Doc) (PrettyM Doc)	Occurs failure, i.e infinite type
MismatchFailure (PrettyM Doc) (PrettyM Doc)

Instances

Show Err Source #
Instance details Defined in Language.PTS.Error Methods showsPrec :: Int -> Err -> ShowS Source # show :: Err -> String Source # showList :: [Err] -> ShowS Source #
IsString Err Source #
Instance details Defined in Language.PTS.Error Methods fromString :: String -> Err Source #
Exception Err Source #
Instance details Defined in Language.PTS.Error Methods toException :: Err -> SomeException Source # fromException :: SomeException -> Maybe Err Source # displayException :: Err -> String Source #
PrettyPrec Err Source #
Instance details Defined in Language.PTS.Error Methods ppp :: Prec -> Err -> PrettyM Doc Source #
AsErr Err Source #
Instance details Defined in Language.PTS.Error Methods _Err :: Prism' Err Err Source #
(PrettyPrec1 t, PrettyPrec v) => Fallible t v Err Source #
Instance details Defined in Language.PTS.Error Methods occursFailure :: v -> UTerm t v -> Err mismatchFailure :: t (UTerm t v) -> t (UTerm t v) -> Err
Monad m => MonadError Err (ScriptT s m) #
Instance details Defined in Language.PTS.Script Methods throwError :: Err -> ScriptT s m a Source # catchError :: ScriptT s m a -> (Err -> ScriptT s m a) -> ScriptT s m a Source #

class AsErr e where Source #

Minimal complete definition

Methods

_Err :: Prism' e Err Source #

Instances

AsErr Err Source #
Instance details Defined in Language.PTS.Error Methods _Err :: Prism' Err Err Source #