Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.Errors

Contents

Generic Error Type
Error with Source Context
Subtyping Obligation Type
Panic (unexpected failures)
Printing Errors
SrcSpan Helpers

Description

This module contains the *types* related creating Errors. It depends only on Fixpoint and basic haskell libraries, and hence, should be importable everywhere.

Synopsis

Generic Error Type

data TError t Source

Generic Type for Error Messages -------------------------------------------

INVARIANT : all Error constructors should have a pos field

Constructors

ErrSubType	liquid type error
Fields pos :: !SrcSpan haskell type location msg :: !Doc ctx :: !(HashMap Symbol t) tact :: !t texp :: !t
ErrFCrash	liquid type error
Fields pos :: !SrcSpan haskell type location msg :: !Doc ctx :: !(HashMap Symbol t) tact :: !t texp :: !t
ErrAssType	condition failure error
Fields pos :: !SrcSpan haskell type location obl :: !Oblig msg :: !Doc ctx :: !(HashMap Symbol t) cond :: t
ErrParse	specification parse error
Fields pos :: !SrcSpan haskell type location msg :: !Doc pErr :: !ParseError
ErrTySpec	sort error in specification
Fields pos :: !SrcSpan haskell type location var :: !Doc typ :: !t msg :: !Doc
ErrTermSpec	sort error in specification
Fields pos :: !SrcSpan haskell type location var :: !Doc exp :: !Expr msg :: !Doc
ErrDupAlias	multiple alias with same name error
Fields pos :: !SrcSpan haskell type location var :: !Doc kind :: !Doc locs :: ![SrcSpan]
ErrDupSpecs	multiple specs for same binder error
Fields pos :: !SrcSpan haskell type location var :: !Doc locs :: ![SrcSpan]
ErrDupMeas	multiple definitions of the same measure
Fields pos :: !SrcSpan haskell type location var :: !Doc tycon :: !Doc locs :: ![SrcSpan]
ErrBadData	bad data type specification (?)
Fields pos :: !SrcSpan haskell type location var :: !Doc msg :: !Doc
ErrDataCon	refined datacon mismatches haskell datacon
Fields pos :: !SrcSpan haskell type location var :: !Doc msg :: !Doc
ErrInvt	Invariant sort error
Fields pos :: !SrcSpan haskell type location inv :: !t msg :: !Doc
ErrIAl	Using sort error
Fields pos :: !SrcSpan haskell type location inv :: !t msg :: !Doc
ErrIAlMis	Incompatible using error
Fields pos :: !SrcSpan haskell type location tAs :: !t tUs :: !t msg :: !Doc
ErrMeas	Measure sort error
Fields pos :: !SrcSpan haskell type location ms :: !Doc msg :: !Doc
ErrHMeas	Haskell bad Measure error
Fields pos :: !SrcSpan haskell type location ms :: !Doc msg :: !Doc
ErrUnbound	Unbound symbol in specification
Fields pos :: !SrcSpan haskell type location var :: !Doc
ErrGhc	GHC error: parsing or type checking
Fields pos :: !SrcSpan haskell type location msg :: !Doc
ErrMismatch	Mismatch between Liquid and Haskell types
Fields pos :: !SrcSpan haskell type location var :: !Doc hs :: !Doc lq :: !Doc lqPos :: !SrcSpan lq type location
ErrPartPred	Mismatch in expected/actual args of abstract refinement
Fields pos :: !SrcSpan haskell type location ectr :: !Doc var :: !Doc argN :: !Int expN :: !Int actN :: !Int
ErrAliasCycle	Cyclic Refined Type Alias Definitions
Fields pos :: !SrcSpan haskell type location acycle :: ![(SrcSpan, Doc)]
ErrIllegalAliasApp	Illegal RTAlias application (from BSort, eg. in PVar)
Fields pos :: !SrcSpan haskell type location dname :: !Doc dpos :: !SrcSpan
ErrAliasApp
Fields pos :: !SrcSpan haskell type location nargs :: !Int dname :: !Doc dpos :: !SrcSpan dargs :: !Int
ErrSaved	Previously saved error, that carries over after DiffCheck
Fields pos :: !SrcSpan haskell type location msg :: !Doc
ErrTermin	Termination Error
Fields pos :: !SrcSpan haskell type location bind :: ![Doc] msg :: !Doc
ErrRClass	Refined Class/Interfaces Conflict
Fields pos :: !SrcSpan haskell type location cls :: !Doc insts :: ![(SrcSpan, Doc)]
ErrBadQual	Non well sorted Qualifier
Fields pos :: !SrcSpan haskell type location qname :: !Doc msg :: !Doc
ErrOther	Sigh. Other.
Fields pos :: SrcSpan haskell type location msg :: !Doc

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

data CtxError t Source

Context information for Error Messages ------------------------------------

Constructors

CtxError
Fields ctErr :: TError t ctCtx :: Doc

Instances

Functor CtxError Source
Eq (CtxError t) Source
Ord (CtxError t) Source

errorWithContext :: TError t -> IO (CtxError t) Source

Subtyping Obligation Type

data Oblig Source

Different kinds of Check Obligations ------------------------------------

Constructors

OTerm	Obligation that proves termination
OInv	Obligation that proves invariants
OCons	Obligation that proves subtyping constraints

Instances

Data Oblig Source
Show Oblig Source
Generic Oblig Source
NFData Oblig Source
PPrint Oblig Source
type Rep Oblig Source

Panic (unexpected failures)

type UserError = TError Doc Source

Simple unstructured type for panic ----------------------------------------

panic :: Maybe SrcSpan -> String -> a Source

Construct and show an Error, then crash

panicDoc :: SrcSpan -> Doc -> a Source

Construct and show an Error, then crash

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

uError :: UserError -> a Source

Construct and show an Error, then crash

Printing Errors

ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc Source

ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc Source

SrcSpan Helpers

realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan Source

unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int) Source