| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Types.Errors
Contents
Description
This module contains the *types* related creating Errors. It depends only on Fixpoint and basic haskell libraries, and hence, should be importable everywhere.
- data TError t
- = ErrSubType { }
- | ErrSubTypeModel { }
- | ErrFCrash { }
- | ErrAssType { }
- | ErrParse { }
- | ErrTySpec { }
- | ErrTermSpec { }
- | ErrDupAlias { }
- | ErrDupSpecs { }
- | ErrDupIMeas { }
- | ErrDupMeas { }
- | ErrDupField { }
- | ErrDupNames { }
- | ErrBadData { }
- | ErrDataCon { }
- | ErrInvt { }
- | ErrIAl { }
- | ErrIAlMis { }
- | ErrMeas { }
- | ErrHMeas { }
- | ErrUnbound { }
- | ErrUnbPred { }
- | ErrGhc { }
- | ErrMismatch { }
- | ErrPartPred { }
- | ErrAliasCycle { }
- | ErrIllegalAliasApp { }
- | ErrAliasApp { }
- | ErrTermin { }
- | ErrRClass { }
- | ErrBadQual { }
- | ErrSaved { }
- | ErrFilePragma { }
- | ErrTyCon { }
- | ErrLiftExp { }
- | ErrParseAnn { }
- | ErrOther { }
- data CtxError t = CtxError {}
- errorWithContext :: TError Doc -> IO (CtxError Doc)
- data Oblig
- data WithModel t
- dropModel :: WithModel t -> t
- type UserError = TError Doc
- panic :: Maybe SrcSpan -> String -> a
- panicDoc :: SrcSpan -> Doc -> a
- todo :: Maybe SrcSpan -> String -> a
- impossible :: Maybe SrcSpan -> String -> a
- uError :: UserError -> a
- ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
- ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc
- realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan
- unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int)
Generic Error Type
Generic Type for Error Messages -------------------------------------------
INVARIANT : all Error constructors should have a pos field
Constructors
| ErrSubType | liquid type error |
| ErrSubTypeModel | liquid type error with a counter-example |
| ErrFCrash | liquid type error |
| ErrAssType | condition failure error |
| ErrParse | specification parse error |
| ErrTySpec | sort error in specification |
| ErrTermSpec | sort error in specification |
| ErrDupAlias | multiple alias with same name error |
| ErrDupSpecs | multiple specs for same binder error |
| ErrDupIMeas | multiple definitions of the same instance measure |
| ErrDupMeas | multiple definitions of the same measure |
| ErrDupField | duplicate fields in same datacon |
| ErrDupNames | name resolves to multiple possible GHC vars |
| ErrBadData | bad data type specification (?) |
| ErrDataCon | refined datacon mismatches haskell datacon |
| ErrInvt | Invariant sort error |
| ErrIAl | Using sort error |
| ErrIAlMis | Incompatible using error |
| ErrMeas | Measure sort error |
| ErrHMeas | Haskell bad Measure error |
| ErrUnbound | Unbound symbol in specification |
| ErrUnbPred | Unbound predicate being applied |
| ErrGhc | GHC error: parsing or type checking |
| ErrMismatch | Mismatch between Liquid and Haskell types |
| ErrPartPred | Mismatch in expected/actual args of abstract refinement |
| ErrAliasCycle | Cyclic Refined Type Alias Definitions |
| ErrIllegalAliasApp | Illegal RTAlias application (from BSort, eg. in PVar) |
| ErrAliasApp | |
| ErrTermin | Termination Error |
| ErrRClass | Refined Class/Interfaces Conflict |
| ErrBadQual | Non well sorted Qualifier |
| ErrSaved | Previously saved error, that carries over after DiffCheck |
| ErrFilePragma | |
| ErrTyCon | |
| ErrLiftExp | |
| ErrParseAnn | |
| ErrOther | Sigh. Other. |
Instances
| Functor TError Source # | |
| Show UserError Source # | |
| Exception UserError Source # | |
| PPrint UserError Source # | |
| Result UserError Source # | |
| Result Error Source # | |
| Eq (TError a) Source # | |
| Ord (TError a) Source # | |
| Generic (TError t) Source # | |
| (PPrint a, Show a) => ToJSON (TError a) Source # | |
| FromJSON (TError a) Source # | |
| Result [Error] Source # | |
| type Rep (TError t) Source # | |
Error with Source Context
Context information for Error Messages ------------------------------------
Subtyping Obligation Type
Different kinds of Check Obligations ------------------------------------
Adding a Model of the context
Panic (unexpected failures)
type UserError = TError Doc Source #
Simple unstructured type for panic ----------------------------------------
todo :: Maybe SrcSpan -> String -> a Source #
Construct and show an Error with an optional SrcSpan, then crash This function should be used to mark unimplemented functionality
impossible :: Maybe SrcSpan -> String -> a Source #
Construct and show an Error with an optional SrcSpan, then crash This function should be used to mark impossible-to-reach codepaths
Printing Errors
SrcSpan Helpers
realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan Source #
unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int) Source #