Language.Haskell.Liquid.Types

Options

data Config

class HasConfig t

hasOpt

Ghc Information

data GhcInfo

data GhcSpec

data TargetVars

Located Things

data Located a

dummyLoc

Symbols

type LocSymbol

type LocText

Default unknown name

dummyName

isDummy

Bare Type Constructors and Variables

data BTyCon

mkBTyCon

mkClassBTyCon

mkPromotedBTyCon

isClassBTyCon

data BTyVar

Refined Type Constructors

data RTyCon

data TyConInfo

defaultTyConInfo

rTyConPVs

rTyConPropVs

isClassRTyCon

isClassType

isEqType

isRVar

isBool

Refinement Types

data RType c tv r

data Ref τ t

type RTProp c tv r

rPropP

data RTyVar

data RTAlias x a

type OkRT c tv r

lmapEAlias

Worlds

data HSeg t

data World t

Classes describing operations on RTypes

class TyConable c

class SubsTy tv ty a

Type Variables

data RTVar tv s

data RTVInfo s

makeRTVar

mapTyVarValue

dropTyVarInfo

rTVarToBind

Predicate Variables

data PVar t

isPropPV

pvType

data PVKind t

data Predicate

Refinements

data UReft r

Parse-time entities describing refined data types

data SizeFun

szFun

data DataDecl

data DataConP

data TyConP

Pre-instantiated RType

type RRType

type RRProp r

type BRType

type BRProp r

type BSort

type BPVar

type RTVU c tv

type PVU c tv

Instantiated RType

type BareType

type PrType

type SpecType

type SpecProp

type LocBareType

type LocSpecType

type RSort

type UsedPVar

type RPVar

type RReft

data REnv

Constructing & Destructing RTypes

data RTypeRep c tv r

fromRTypeRep

toRTypeRep

mkArrow

bkArrowDeep

bkArrow

safeBkArrow

mkUnivs

bkUniv

bkClass

rFun

rCls

rRCls

Manipulating Predicates

pvars

pappSym

pApp

Some tests on RTypes

isBase

isFunTy

isTrivial

Traversing RType

efoldReft

foldReft

foldReft'

mapReft

mapReftM

mapPropM

mapBot

mapBind

???

data Oblig

ignoreOblig

addInvCond

Inferred Annotations

data AnnInfo a

data Annot t

Overall Output

data Output a

Refinement Hole

hole

isHole

hasHole

Converting To and From Sort

ofRSort

toRSort

rTypeValueVar

rTypeReft

stripRTypeBase

topRTypeBase

Class for values that can be pretty printed

class PPrint a

pprint

showpp

Printer Configuration

data PPEnv

ppEnv

ppEnvShort

Modules and Imports

data ModName

data ModType

isSrcImport

isSpecImport

getModName

getModString

Refinement Type Aliases

data RTEnv

mapRT

mapRE

Errors and Error Messages

type Error

type ErrorResult

Source information (associated with constraints)

data Cinfo

Measures

data Measure ty ctor

data CMeasure ty

data Def ty ctor

data Body

data MSpec ty ctor

Type Classes

data RClass ty

KV Profiling

data KVKind

data KVProf

emptyKVProf

updKVProf

Misc

mapRTAVars

insertsSEnv

Strata

data Stratum

type Strata

isSVar

getStrata

makeDivType

makeFinType

CoreToLogic

data LogicMap

toLogicMap

eAppWithMap

data LMap

Refined Instances

type RDEnv

data DEnv x ty

data RInstance t

data RISig t

Ureftable Instances

class UReftable r

String Literals

liquidBegin

liquidEnd

data Axiom b s e

type HAxiom

data AxiomEq

rtyVarUniqueSymbol

tyVarUniqueSymbol

rtyVarType