liquidhaskell-0.8.10.1: Liquid Types for Haskell
Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Types.Errors

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 #

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

INVARIANT : all Error constructors should have a pos field

Constructors

ErrSubType

liquid type error

Fields

ErrSubTypeModel

liquid type error with a counter-example

Fields

ErrFCrash

liquid type error

Fields

ErrHole

hole type

Fields

ErrHoleCycle

hole dependencies form a cycle error

Fields

ErrAssType

condition failure error

Fields

ErrParse

specification parse error

Fields

ErrTySpec

sort error in specification

Fields

ErrTermSpec

sort error in specification

Fields

ErrDupAlias

multiple alias with same name error

Fields

ErrDupSpecs

multiple specs for same binder error

Fields

ErrDupIMeas

multiple definitions of the same instance measure

Fields

ErrDupMeas

multiple definitions of the same measure

Fields

ErrDupField

duplicate fields in same datacon

Fields

ErrDupNames

name resolves to multiple possible GHC vars

Fields

ErrBadData

bad data type specification (?)

Fields

ErrBadGADT

bad data type specification (?)

Fields

ErrDataCon

refined datacon mismatches haskell datacon

Fields

ErrInvt

Invariant sort error

Fields

ErrIAl

Using sort error

Fields

ErrIAlMis

Incompatible using error

Fields

ErrMeas

Measure sort error

Fields

ErrHMeas

Haskell bad Measure error

Fields

ErrUnbound

Unbound symbol in specification

Fields

ErrUnbPred

Unbound predicate being applied

Fields

ErrGhc

GHC error: parsing or type checking

Fields

ErrResolve

Name resolution error

Fields

ErrMismatch

Mismatch between Liquid and Haskell types

Fields

ErrPartPred

Mismatch in expected/actual args of abstract refinement

Fields

ErrAliasCycle

Cyclic Refined Type Alias Definitions

Fields

ErrIllegalAliasApp

Illegal RTAlias application (from BSort, eg. in PVar)

Fields

ErrAliasApp 

Fields

ErrTermin

Termination Error

Fields

ErrStTerm

Termination Error

Fields

ErrILaw

Instance Law Error

Fields

ErrRClass

Refined Class/Interfaces Conflict

Fields

ErrMClass

Standalone class method refinements

Fields

ErrBadQual

Non well sorted Qualifier

Fields

ErrSaved

Previously saved error, that carries over after DiffCheck

Fields

ErrFilePragma 

Fields

ErrTyCon 

Fields

ErrLiftExp 

Fields

ErrParseAnn 

Fields

ErrNoSpec 

Fields

ErrFail 

Fields

ErrFailUsed 

Fields

ErrRewrite 

Fields

ErrOther

Sigh. Other.

Fields

Instances

Instances details
Functor TError # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

fmap :: (a -> b) -> TError a -> TError b #

(<$) :: a -> TError b -> TError a #

Show UserError # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Show Error # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Exception UserError # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Exception Error # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint UserError # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> UserError -> Doc #

pprintPrec :: Int -> Tidy -> UserError -> Doc #

PPrint Error # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

pprintPrec :: Int -> Tidy -> Error -> Doc #

FromJSON ErrorResult 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

Methods

parseJSON :: Value -> Parser ErrorResult

parseJSONList :: Value -> Parser [ErrorResult]

ToJSON ErrorResult 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

Methods

toJSON :: ErrorResult -> Value

toEncoding :: ErrorResult -> Encoding

toJSONList :: [ErrorResult] -> Value

toEncodingList :: [ErrorResult] -> Encoding

Result UserError # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

result :: UserError -> FixResult UserError #

Result Error # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

result :: Error -> FixResult UserError #

Eq (TError a) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

(==) :: TError a -> TError a -> Bool #

(/=) :: TError a -> TError a -> Bool #

Ord (TError a) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

compare :: TError a -> TError a -> Ordering #

(<) :: TError a -> TError a -> Bool #

(<=) :: TError a -> TError a -> Bool #

(>) :: TError a -> TError a -> Bool #

(>=) :: TError a -> TError a -> Bool #

max :: TError a -> TError a -> TError a #

min :: TError a -> TError a -> TError a #

Generic (TError t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Associated Types

type Rep (TError t) :: Type -> Type #

Methods

from :: TError t -> Rep (TError t) x #

to :: Rep (TError t) x -> TError t #

NFData a => NFData (TError a) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: TError a -> () #

Exception [Error] # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

FromJSON (TError a) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

parseJSON :: Value -> Parser (TError a)

parseJSONList :: Value -> Parser [TError a]

(PPrint a, Show a) => ToJSON (TError a) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

toJSON :: TError a -> Value

toEncoding :: TError a -> Encoding

toJSONList :: [TError a] -> Value

toEncodingList :: [TError a] -> Encoding

Result [Error] # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

result :: [Error] -> FixResult UserError #

type Rep (TError t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

type Rep (TError t) = D1 ('MetaData "TError" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.10.1-inplace" 'False) (((((C1 ('MetaCons "ErrSubType" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "ctx") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap Symbol t)) :*: (S1 ('MetaSel ('Just "tact") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Just "texp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)))) :+: (C1 ('MetaCons "ErrSubTypeModel" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "ctxM") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap Symbol (WithModel t))) :*: (S1 ('MetaSel ('Just "tactM") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (WithModel t)) :*: S1 ('MetaSel ('Just "texp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)))) :+: C1 ('MetaCons "ErrFCrash" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "ctx") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap Symbol t)) :*: (S1 ('MetaSel ('Just "tact") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Just "texp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)))))) :+: (C1 ('MetaCons "ErrHole" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "ctx") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap Symbol t)) :*: (S1 ('MetaSel ('Just "svar") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "thl") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)))) :+: (C1 ('MetaCons "ErrHoleCycle" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "holesCycle") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol])) :+: C1 ('MetaCons "ErrAssType" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "obl") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Oblig)) :*: (S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: (S1 ('MetaSel ('Just "ctx") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap Symbol t)) :*: S1 ('MetaSel ('Just "cond") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))))))) :+: ((C1 ('MetaCons "ErrParse" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "pErr") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ParseError))) :+: (C1 ('MetaCons "ErrTySpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "knd") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Doc))) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: (S1 ('MetaSel ('Just "typ") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)))) :+: C1 ('MetaCons "ErrTermSpec" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :*: (S1 ('MetaSel ('Just "exp") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: (S1 ('MetaSel ('Just "typ") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Just "msg'") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)))))) :+: (C1 ('MetaCons "ErrDupAlias" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "kind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "locs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SrcSpan]))) :+: (C1 ('MetaCons "ErrDupSpecs" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "locs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SrcSpan]))) :+: C1 ('MetaCons "ErrDupIMeas" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "tycon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "locs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SrcSpan]))))))) :+: (((C1 ('MetaCons "ErrDupMeas" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "locs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SrcSpan]))) :+: (C1 ('MetaCons "ErrDupField" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "dcon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "field") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrDupNames" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "names") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Doc]))))) :+: (C1 ('MetaCons "ErrBadData" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: (C1 ('MetaCons "ErrBadGADT" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrDataCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)))))) :+: ((C1 ('MetaCons "ErrInvt" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "inv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: (C1 ('MetaCons "ErrIAl" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "inv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrIAlMis" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "tAs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t)) :*: (S1 ('MetaSel ('Just "tUs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 t) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))))) :+: (C1 ('MetaCons "ErrMeas" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "ms") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: (C1 ('MetaCons "ErrHMeas" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "ms") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrUnbound" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))))))) :+: ((((C1 ('MetaCons "ErrUnbPred" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :+: (C1 ('MetaCons "ErrGhc" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :+: C1 ('MetaCons "ErrResolve" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "kind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))))) :+: (C1 ('MetaCons "ErrMismatch" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :*: ((S1 ('MetaSel ('Just "hs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "lqTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "diff") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe (Doc, Doc))) :*: S1 ('MetaSel ('Just "lqPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan)))) :+: (C1 ('MetaCons "ErrPartPred" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "ectr") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :*: (S1 ('MetaSel ('Just "argN") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Just "expN") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "actN") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))) :+: C1 ('MetaCons "ErrAliasCycle" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "acycle") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(SrcSpan, Doc)]))))) :+: ((C1 ('MetaCons "ErrIllegalAliasApp" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "dname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "dpos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan))) :+: (C1 ('MetaCons "ErrAliasApp" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "dname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "dpos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrTermin" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "bind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Doc]) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))))) :+: (C1 ('MetaCons "ErrStTerm" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "dname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: (C1 ('MetaCons "ErrILaw" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "cname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :*: (S1 ('MetaSel ('Just "iname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrRClass" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "cls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "insts") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(SrcSpan, Doc)]))))))) :+: (((C1 ('MetaCons "ErrMClass" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :+: (C1 ('MetaCons "ErrBadQual" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "qname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrSaved" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "nam") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))))) :+: (C1 ('MetaCons "ErrFilePragma" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan)) :+: (C1 ('MetaCons "ErrTyCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "tcname") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrLiftExp" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))))) :+: ((C1 ('MetaCons "ErrParseAnn" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :+: (C1 ('MetaCons "ErrNoSpec" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "srcF") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "bspF") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))) :+: C1 ('MetaCons "ErrFail" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)))) :+: (C1 ('MetaCons "ErrFailUsed" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: (S1 ('MetaSel ('Just "var") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Just "clients") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Doc]))) :+: (C1 ('MetaCons "ErrRewrite" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc)) :+: C1 ('MetaCons "ErrOther" 'PrefixI 'True) (S1 ('MetaSel ('Just "pos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SrcSpan) :*: S1 ('MetaSel ('Just "msg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc))))))))

Error with Source Context

data CtxError t #

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

Constructors

CtxError 

Fields

Instances

Instances details
Functor CtxError # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

fmap :: (a -> b) -> CtxError a -> CtxError b #

(<$) :: a -> CtxError b -> CtxError a #

Eq (CtxError t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

(==) :: CtxError t -> CtxError t -> Bool #

(/=) :: CtxError t -> CtxError t -> Bool #

Ord (CtxError t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

compare :: CtxError t -> CtxError t -> Ordering #

(<) :: CtxError t -> CtxError t -> Bool #

(<=) :: CtxError t -> CtxError t -> Bool #

(>) :: CtxError t -> CtxError t -> Bool #

(>=) :: CtxError t -> CtxError t -> Bool #

max :: CtxError t -> CtxError t -> CtxError t #

min :: CtxError t -> CtxError t -> CtxError t #

Show (CtxError Doc) # 
Instance details

Defined in Language.Haskell.Liquid.UX.CmdLine

PPrint (CtxError Doc) #

Pretty Printing Error Messages --------------------------------------------

Need to put PPrint Error instance here (instead of in Types), as it depends on PPrint SpecTypes, which lives in this module.

Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> CtxError Doc -> Doc #

pprintPrec :: Int -> Tidy -> CtxError Doc -> Doc #

PPrint (CtxError SpecType) # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> CtxError SpecType -> Doc #

pprintPrec :: Int -> Tidy -> CtxError SpecType -> Doc #

Subtyping Obligation Type

data Oblig #

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

Constructors

OTerm

Obligation that proves termination

OInv

Obligation that proves invariants

OCons

Obligation that proves subtyping constraints

Instances

Instances details
Eq Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

(==) :: Oblig -> Oblig -> Bool #

(/=) :: Oblig -> Oblig -> Bool #

Data Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Oblig -> c Oblig #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Oblig #

toConstr :: Oblig -> Constr #

dataTypeOf :: Oblig -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Oblig) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Oblig) #

gmapT :: (forall b. Data b => b -> b) -> Oblig -> Oblig #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r #

gmapQ :: (forall d. Data d => d -> u) -> Oblig -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Oblig -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig #

Show Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

showsPrec :: Int -> Oblig -> ShowS #

show :: Oblig -> String #

showList :: [Oblig] -> ShowS #

Generic Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Associated Types

type Rep Oblig :: Type -> Type #

Methods

from :: Oblig -> Rep Oblig x #

to :: Rep Oblig x -> Oblig #

NFData Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

rnf :: Oblig -> () #

Binary Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

put :: Oblig -> Put #

get :: Get Oblig #

putList :: [Oblig] -> Put #

PPrint Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> Oblig -> Doc #

pprintPrec :: Int -> Tidy -> Oblig -> Doc #

Hashable Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

hashWithSalt :: Int -> Oblig -> Int

hash :: Oblig -> Int

type Rep Oblig # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "OTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OInv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OCons" 'PrefixI 'False) (U1 :: Type -> Type)))

Adding a Model of the context

data WithModel t #

Constructors

NoModel t 
WithModel !Doc t 

Instances

Instances details
Functor WithModel # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

fmap :: (a -> b) -> WithModel a -> WithModel b #

(<$) :: a -> WithModel b -> WithModel a #

Eq t => Eq (WithModel t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

(==) :: WithModel t -> WithModel t -> Bool #

(/=) :: WithModel t -> WithModel t -> Bool #

Show t => Show (WithModel t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Generic (WithModel t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Associated Types

type Rep (WithModel t) :: Type -> Type #

Methods

from :: WithModel t -> Rep (WithModel t) x #

to :: Rep (WithModel t) x -> WithModel t #

NFData t => NFData (WithModel t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

rnf :: WithModel t -> () #

Subable t => Subable (WithModel t) 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

syms :: WithModel t -> [Symbol]

substa :: (Symbol -> Symbol) -> WithModel t -> WithModel t

substf :: (Symbol -> Expr) -> WithModel t -> WithModel t

subst :: Subst -> WithModel t -> WithModel t

subst1 :: WithModel t -> (Symbol, Expr) -> WithModel t

type Rep (WithModel t) # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

type Rep (WithModel t) = D1 ('MetaData "WithModel" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "NoModel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "WithModel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

Panic (unexpected failures)

type UserError = TError Doc #

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

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

Construct and show an Error, then crash

panicDoc :: SrcSpan -> Doc -> a #

Construct and show an Error, then crash

todo :: Maybe SrcSpan -> String -> a #

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 #

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 #

Construct and show an Error, then crash

sourceErrors :: String -> SourceError -> [TError t] #

Convert a GHC error into a list of our errors.

errDupSpecs :: Doc -> ListNE SrcSpan -> TError t #

Printing Errors

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

ppTicks :: PPrint a => a -> Doc #

SrcSpan Helpers

Orphan instances

NFData ParseError # 
Instance details

Methods

rnf :: ParseError -> () #

PPrint SrcSpan # 
Instance details

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc #

pprintPrec :: Int -> Tidy -> SrcSpan -> Doc #

PPrint ParseError # 
Instance details

Methods

pprintTidy :: Tidy -> ParseError -> Doc #

pprintPrec :: Int -> Tidy -> ParseError -> Doc #

FromJSON RealSrcSpan # 
Instance details

Methods

parseJSON :: Value -> Parser RealSrcSpan

parseJSONList :: Value -> Parser [RealSrcSpan]

FromJSON SrcSpan # 
Instance details

Methods

parseJSON :: Value -> Parser SrcSpan

parseJSONList :: Value -> Parser [SrcSpan]

FromJSONKey SrcSpan # 
Instance details

Methods

fromJSONKey :: FromJSONKeyFunction SrcSpan

fromJSONKeyList :: FromJSONKeyFunction [SrcSpan]

ToJSON RealSrcSpan # 
Instance details

Methods

toJSON :: RealSrcSpan -> Value

toEncoding :: RealSrcSpan -> Encoding

toJSONList :: [RealSrcSpan] -> Value

toEncodingList :: [RealSrcSpan] -> Encoding

ToJSON SrcSpan # 
Instance details

Methods

toJSON :: SrcSpan -> Value

toEncoding :: SrcSpan -> Encoding

toJSONList :: [SrcSpan] -> Value

toEncodingList :: [SrcSpan] -> Encoding

ToJSONKey SrcSpan # 
Instance details

Methods

toJSONKey :: ToJSONKeyFunction SrcSpan

toJSONKeyList :: ToJSONKeyFunction [SrcSpan]