liquidhaskell-0.8.10.2: 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 Source #

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 Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

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

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

Show UserError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Show Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

ToJSON ErrorResult Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

FromJSON ErrorResult Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.DiffCheck

Exception UserError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Exception Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

PPrint UserError Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

PPrint Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Methods

pprintTidy :: Tidy -> Error -> Doc #

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

Result UserError Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Result Error Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Eq (TError a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

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

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

Ord (TError a) Source # 
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) Source # 
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) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

rnf :: TError a -> () #

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

Defined in Language.Haskell.Liquid.Types.Errors

FromJSON (TError a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Exception [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

Result [Error] Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

type Rep (TError t) Source # 
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.2-L92dB1QZcuO9sqg2FFZRKf" '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 Source #

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

Constructors

CtxError 

Fields

Instances

Instances details
Functor CtxError Source # 
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) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

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

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

Ord (CtxError t) Source # 
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) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.CmdLine

PPrint (CtxError Doc) Source #

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

PPrint (CtxError SpecType) Source # 
Instance details

Defined in Language.Haskell.Liquid.UX.Tidy

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

Instances details
Eq Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

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

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

Data Oblig Source # 
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 Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

showsPrec :: Int -> Oblig -> ShowS #

show :: Oblig -> String #

showList :: [Oblig] -> ShowS #

Generic Oblig Source # 
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 Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

rnf :: Oblig -> () #

Binary Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

put :: Oblig -> Put #

get :: Get Oblig #

putList :: [Oblig] -> Put #

Hashable Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

hashWithSalt :: Int -> Oblig -> Int #

hash :: Oblig -> Int #

PPrint Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

pprintTidy :: Tidy -> Oblig -> Doc #

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

type Rep Oblig Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" '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 Source #

Constructors

NoModel t 
WithModel !Doc t 

Instances

Instances details
Functor WithModel Source # 
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) Source # 
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) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Generic (WithModel t) Source # 
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) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Errors

Methods

rnf :: WithModel t -> () #

Subable t => Subable (WithModel t) Source # 
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) Source # 
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.2-L92dB1QZcuO9sqg2FFZRKf" '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 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

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

Convert a GHC error into a list of our errors.

Printing Errors

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

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

SrcSpan Helpers

Orphan instances