Language.Haskell.Liquid.Types.Bounds

Documentation

data Bound t e

Constructors

Bound

Fields

bname :: LocSymbol

The name of the bound

tyvars :: [t]

Type variables that appear in the bounds

bparams :: [(LocSymbol, t)]

These are abstract refinements, for now

bargs :: [(LocSymbol, t)]

These are value variables

bbody :: e

The body of the bound

Instances

Bifunctor Bound

Eq (Bound t e)

(PPrint e, PPrint t) => Show (Bound t e)

Hashable (Bound t e)

(PPrint e, PPrint t) => PPrint (Bound t e)

type RBound = RRBound RSort

type RRBound tv = Bound tv Expr

type RBEnv = HashMap LocSymbol RBound

type RRBEnv tv = HashMap LocSymbol (RRBound tv)

makeBound :: (PPrint r, UReftable r) => RRBound RSort -> [RRType r] -> [Symbol] -> RRType r -> RRType r