Language.Haskell.Liquid.Types.RefType

Functions for lifting Reft-values to Spec-values

uTop

uReft

uRType

uRType'

uRTypeGen

uPVar

Applying a solution to a SpecType

applySolution

Functions for decreasing arguments

isDecreasing

makeDecrType

makeNumEnv

makeLexRefa

Functions for manipulating Predicates

pdVar

findPVar

class FreeVar a v

freeTyVars

tyClasses

tyConName

Quantifying RTypes

quantifyRTy

quantifyFreeRTy

RType constructors

ofType

toType

bareOfType

bTyVar

rTyVar

rVar

rApp

rEx

symbolRTyVar

bareRTyVar

tyConBTyCon

Substitutions

subts

subvPredicate

subvUReft

subsTyVar_meet

subsTyVar_meet'

subsTyVar_nomeet

subsTyVars_nomeet

subsTyVars_meet

Destructors

addTyConInfo

appRTyCon

typeUniqueSymbol

classBinds

isSizeable

Manipulating Refinements in RTypes

strengthen

generalize

normalizePds

dataConMsReft

dataConReft

rTypeSortedReft

rTypeSort

typeSort

shiftVV

TODO: classify these

mkDataConIdsTy

mkTyConInfo

meetable

strengthenRefTypeGen

strengthenDataConType

isBaseTy

updateRTVar

isValKind

kindToRType

rTVarInfo