Language.Haskell.Liquid.Types.RefType

Refinement Types. Mostly mirroring the GHC Type definition, but with room for refinements of various sorts. TODO: Desperately needs re-organization.

Documentation

data TyConMap

Information about Type Constructors

Instances

Qualify TyConMap

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConMap -> TyConMap

Functions for lifting Reft-values to Spec-values

uTop :: r -> UReft r

uReft :: (Symbol, Expr) -> UReft Reft

uRType :: RType c tv a -> RType c tv (UReft a)

Various functions for converting vanilla Reft to Spec

uRType' :: RType c tv (UReft a) -> RType c tv a

uRTypeGen :: Reftable b => RType c tv a -> RType c tv b

uPVar :: PVar t -> UsedPVar

Applying a solution to a SpecType

applySolution :: Functor f => FixSolution -> f SpecType -> f SpecType

Functions for decreasing arguments

isDecreasing :: HashSet TyCon -> [RTyVar] -> SpecType -> Bool

makeDecrType :: Symbolic a => HashSet TyCon -> Maybe (a, (Symbol, RType RTyCon t (UReft Reft))) -> Either (Symbol, RType RTyCon t (UReft Reft)) String

makeNumEnv :: (Foldable t, TyConable c) => t (RType c b t1) -> [b]

Termination Predicates ----------------------------------------------------

makeLexRefa :: [Located Expr] -> [Located Expr] -> UReft Reft

Functions for manipulating Predicates

pdVar :: PVar t -> Predicate

findPVar :: [PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())

class FreeVar a v

Minimal complete definition

freeVars

Instances

FreeVar BTyCon BTyVar

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: BTyCon -> [BTyVar]

FreeVar RTyCon RTyVar

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: RTyCon -> [RTyVar]

allTyVars :: Ord tv => RType c tv r -> [tv]

allTyVars' :: Eq tv => RType c tv r -> [tv]

freeTyVars :: Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]

tyClasses :: OkRT RTyCon tv r => RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]

tyConName :: TyCon -> Symbol

Quantifying RTypes

quantifyRTy :: (Monoid r, Eq tv) => [RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r

quantifyFreeRTy :: (Monoid r, Eq tv) => RType c tv r -> RType c tv r

RType constructors

ofType :: Monoid r => Type -> RRType r

toType :: ToTypeable r => Bool -> RRType r -> Type

bareOfType :: Monoid r => Type -> BRType r

bTyVar :: Symbol -> BTyVar

rTyVar :: TyVar -> RTyVar

rVar :: Monoid r => TyVar -> RType c RTyVar r

Helper Functions (RJ: Helping to do what?) --------------------------------

rApp :: TyCon -> [RType RTyCon tv r] -> [RTProp RTyCon tv r] -> r -> RType RTyCon tv r

gApp :: TyCon -> [RTyVar] -> [PVar a] -> SpecType

rEx :: Foldable t => t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r

symbolRTyVar :: Symbol -> RTyVar

bareRTyVar :: BTyVar -> RTyVar

tyConBTyCon :: TyCon -> BTyCon

pdVarReft :: PVar t -> UReft Reft

Substitutions

subts :: SubsTy tv ty c => [(tv, ty)] -> c -> c

Type Substitutions --------------------------------------------------------

subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate

subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft

subsTyVarMeet :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r

subsTyVarMeet' :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv r) -> RType c tv r -> RType c tv r

subsTyVarNoMeet :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r

subsTyVarsNoMeet :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r

subsTyVarsMeet :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r

Destructors

addTyConInfo :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> TyConMap -> RRType r -> RRType r

appRTyCon :: ToTypeable r => TCEmb TyCon -> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar])

NOTE:FamInstPredVars

related to [NOTE:FamInstEmbeds] See testsdataconpos/T1446.hs The function txRefSort converts

Intp ===> {v:Int | p v}

which is fine, but also converts

Fieldq Blob a ===> {v:Field Blob a | q v}

which is NOT ok, because q expects a different arg.

The above happens because, thanks to instance-family stuff, LH doesn't realize that q is actually an ARG of Field Blob Note that Field itself has no args, but Field Blob does...

That is, it is not enough to store the refined TyCon info, solely in the RTyCon as with family instances, you need BOTH the TyCon and the args to determine the extra info.

We do so in TyConMap, and by crucially extending

RefType.appRTyCon whose job is to use the Refined TyCon that is, the RTyCon generated from the TyConP to strengthen individual occurrences of the TyCon applied to various arguments.

typeUniqueSymbol :: Type -> Symbol

classBinds :: TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)]

Binders generated by class predicates, typically for constraining tyvars (e.g. FNum)

isSizeable :: HashSet TyCon -> TyCon -> Bool

famInstTyConType :: TyCon -> Maybe Type

famInstArgs :: TyCon -> Maybe (TyCon, [Type])

famInstArgs c destructs a family-instance TyCon into its components, e.g. e.g. 'famInstArgs R:FieldBlob' is (Field, [Blob])

Manipulating Refinements in RTypes

strengthen :: Reftable r => RType c tv r -> r -> RType c tv r

generalize :: (Eq tv, Monoid r) => RType c tv r -> RType c tv r

normalizePds :: OkRT c tv r => RType c tv r -> RType c tv r

dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft

dataConReft :: DataCon -> [Symbol] -> Reft

rTypeSortedReft :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> RRType r -> SortedReft

NOTE:Hole-Lit

We use toType to convert RType to GHC.Type to expand any GHC related type-aliases, e.g. in Bare.Resolve.expandRTypeSynonyms. If the RType has a RHole then what to do?

We, encode RHole as `LitTy LH_HOLE` -- which is a bit of a *hack*. The only saving grace is it is used *temporarily* and then swiftly turned back into an RHole via ofType (after GHC has done its business of expansion).

Of course, we hope this doesn't break any GHC invariants! See issue #1476 and #1477

The other option is to *not* use toType on things that have holes in them, but this seems worse, e.g. because you may define a plain GHC alias like:

type ToNat a = a -> Nat

and then you might write refinement types like:

and we'd want to expand the above to

and then resolve the hole using the (GHC) type of foo.

Annotations and Solutions -------------------------------------------------

rTypeSort :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> RRType r -> Sort

typeSort :: TCEmb TyCon -> Type -> Sort

From Old Fixpoint ---------------------------------------------------------

shiftVV :: (TyConable c, Reftable (f Reft), Functor f) => RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)

TODO: classify these

expandProductType :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Var -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r

mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo

strengthenRefTypeGen :: (OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => RType c tv r -> RType c tv r -> RType c tv r

strengthenDataConType :: (Var, SpecType) -> (Var, SpecType)

isBaseTy :: Type -> Bool

updateRTVar :: Monoid r => RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)

isValKind :: Kind -> Bool

kindToRType :: Monoid r => Type -> RRType r

rTVarInfo :: Monoid r => TyVar -> RTVInfo (RRType r)

tyVarsPosition :: RType RTyCon tv r -> Positions tv

tyVarsPosition t returns the type variables appearing | (in positive positions, in negative positions, in undetermined positions) | undetermined positions are due to type constructors and type application

data Positions a

Constructors

Pos

Fields

• ppos :: [a]
• pneg :: [a]
• punknown :: [a]

Instances

Monoid (Positions a)

Defined in Language.Haskell.Liquid.Types.RefType

Methods

mempty :: Positions a

mappend :: Positions a -> Positions a -> Positions a

mconcat :: [Positions a] -> Positions a

Semigroup (Positions a)

Defined in Language.Haskell.Liquid.Types.RefType

Methods

(<>) :: Positions a -> Positions a -> Positions a

sconcat :: NonEmpty (Positions a) -> Positions a

stimes :: Integral b => b -> Positions a -> Positions a

isNumeric :: TCEmb TyCon -> RTyCon -> Bool

Orphan instances

Show RTyVar

Printing Refinement Types -------------------------------------------------

Methods

showsPrec :: Int -> RTyVar -> ShowS

show :: RTyVar -> String

showList :: [RTyVar] -> ShowS

Eq RTyVar

Wrappers for GHC Type Elements --------------------------------------------

Methods

(==) :: RTyVar -> RTyVar -> Bool

(/=) :: RTyVar -> RTyVar -> Bool

Ord RTyVar

Methods

compare :: RTyVar -> RTyVar -> Ordering

(<) :: RTyVar -> RTyVar -> Bool

(<=) :: RTyVar -> RTyVar -> Bool

(>) :: RTyVar -> RTyVar -> Bool

(>=) :: RTyVar -> RTyVar -> Bool

max :: RTyVar -> RTyVar -> RTyVar

min :: RTyVar -> RTyVar -> RTyVar

Hashable RTyCon

Methods

hashWithSalt :: Int -> RTyCon -> Int

hash :: RTyCon -> Int

Hashable RTyVar

Methods

hashWithSalt :: Int -> RTyVar -> Int

hash :: RTyVar -> Int

Fixpoint Class

Methods

toFix :: Class -> Doc

simplify :: Class -> Class

Fixpoint String

Methods

toFix :: String -> Doc

simplify :: String -> String

PPrint DataCtor

Methods

pprintTidy :: Tidy -> DataCtor -> Doc

pprintPrec :: Int -> Tidy -> DataCtor -> Doc

PPrint DataDecl

Methods

pprintTidy :: Tidy -> DataDecl -> Doc

pprintPrec :: Int -> Tidy -> DataDecl -> Doc

Expression Var

Converting to Fixpoint ----------------------------------------------------

Methods

expr :: Var -> Expr

SubsTy TyVar Type SpecType

Methods

subt :: (TyVar, Type) -> SpecType -> SpecType

SubsTy Symbol RSort Sort

Methods

subt :: (Symbol, RSort) -> Sort -> Sort

SubsTy BTyVar BSort BSort

Methods

subt :: (BTyVar, BSort) -> BSort -> BSort

SubsTy BTyVar BSort BTyCon

Methods

subt :: (BTyVar, BSort) -> BTyCon -> BTyCon

SubsTy RTyVar RSort Sort

Methods

subt :: (RTyVar, RSort) -> Sort -> Sort

SubsTy RTyVar RSort PrType

Methods

subt :: (RTyVar, RSort) -> PrType -> PrType

SubsTy RTyVar RSort RSort

Methods

subt :: (RTyVar, RSort) -> RSort -> RSort

SubsTy RTyVar RSort RTyCon

Methods

subt :: (RTyVar, RSort) -> RTyCon -> RTyCon

SubsTy RTyVar RSort SpecType

Methods

subt :: (RTyVar, RSort) -> SpecType -> SpecType

SubsTy RTyVar RTyVar SpecType

Methods

subt :: (RTyVar, RTyVar) -> SpecType -> SpecType

SubsTy tv RSort Predicate

Methods

subt :: (tv, RSort) -> Predicate -> Predicate

SubsTy tv ty Symbol

Methods

subt :: (tv, ty) -> Symbol -> Symbol

SubsTy tv ty Sort => SubsTy tv ty Expr

Methods

subt :: (tv, ty) -> Expr -> Expr

SubsTy tv ty Expr => SubsTy tv ty Reft

Methods

subt :: (tv, ty) -> Reft -> Reft

SubsTy tv ty ()

Methods

subt :: (tv, ty) -> () -> ()

SubsTy Symbol Symbol (BRType r)

Methods

subt :: (Symbol, Symbol) -> BRType r -> BRType r

SubsTy tv ty ty => SubsTy tv ty (PVKind ty)

Methods

subt :: (tv, ty) -> PVKind ty -> PVKind ty

SubsTy tv ty ty => SubsTy tv ty (PVar ty)

Methods

subt :: (tv, ty) -> PVar ty -> PVar ty

SubsTy tv ty r => SubsTy tv ty (UReft r)

Methods

subt :: (tv, ty) -> UReft r -> UReft r

(SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b)

Methods

subt :: (tv, ty) -> (a, b) -> (a, b)

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r)

Methods

subt :: (Symbol, Symbol) -> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r))

Methods

subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r)

SubsTy BTyVar (RType BTyCon BTyVar ()) Sort

Methods

subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort

SubsTy BTyVar (RType c BTyVar ()) BTyVar

Methods

subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar

SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar

Methods

subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar

SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ()))

Methods

subt :: (BTyVar, RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ()) -> RTVar BTyVar (RType c BTyVar ())

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ()))

Methods

subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ()) -> RTVar RTyVar (RType RTyCon RTyVar ())

PPrint (UReft r) => Show (UReft r)

Methods

showsPrec :: Int -> UReft r -> ShowS

show :: UReft r -> String

showList :: [UReft r] -> ShowS

Subable (RRProp Reft)

Subable Instances -----------------------------------------------------

Methods

syms :: RRProp Reft -> [Symbol]

substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft

substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft

subst :: Subst -> RRProp Reft -> RRProp Reft

subst1 :: RRProp Reft -> (Symbol, Expr) -> RRProp Reft

(Show tv, Show ty) => Show (RTAlias tv ty)

Auxiliary Stuff Used Elsewhere ---------------------------------------------

Methods

showsPrec :: Int -> RTAlias tv ty -> ShowS

show :: RTAlias tv ty -> String

showList :: [RTAlias tv ty] -> ShowS

(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RTProp c tv r)

Methods

mempty :: RTProp c tv r

mappend :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r

mconcat :: [RTProp c tv r] -> RTProp c tv r

(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Monoid (RType c tv r)

Methods

mempty :: RType c tv r

mappend :: RType c tv r -> RType c tv r -> RType c tv r

mconcat :: [RType c tv r] -> RType c tv r

(SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Semigroup (RTProp c tv r)

Methods

(<>) :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r

sconcat :: NonEmpty (RTProp c tv r) -> RTProp c tv r

stimes :: Integral b => b -> RTProp c tv r -> RTProp c tv r

(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => Semigroup (RType c tv r)

Methods

(<>) :: RType c tv r -> RType c tv r -> RType c tv r

sconcat :: NonEmpty (RType c tv r) -> RType c tv r

stimes :: Integral b => b -> RType c tv r -> RType c tv r

PPrint (RTProp c tv r) => Show (RTProp c tv r)

Methods

showsPrec :: Int -> RTProp c tv r -> ShowS

show :: RTProp c tv r -> String

showList :: [RTProp c tv r] -> ShowS

PPrint (RType c tv r) => Show (RType c tv r)

Methods

showsPrec :: Int -> RType c tv r -> ShowS

show :: RType c tv r -> String

showList :: [RType c tv r] -> ShowS

(Eq c, Eq tv, Hashable tv, PPrint tv, TyConable c, PPrint c, Reftable (RTProp c tv ())) => Eq (RType c tv ())

Methods

(==) :: RType c tv () -> RType c tv () -> Bool

(/=) :: RType c tv () -> RType c tv () -> Bool

Reftable (RTProp BTyCon BTyVar (UReft Reft))

Methods

isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool

ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc

top :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft)

bot :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft)

meet :: RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft) -> RTProp BTyCon BTyVar (UReft Reft)

toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft

ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft)

params :: RTProp BTyCon BTyVar (UReft Reft) -> [Symbol]

Reftable (RTProp BTyCon BTyVar ())

Methods

isTauto :: RTProp BTyCon BTyVar () -> Bool

ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc

top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar ()

bot :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar ()

meet :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar ()

toReft :: RTProp BTyCon BTyVar () -> Reft

ofReft :: Reft -> RTProp BTyCon BTyVar ()

params :: RTProp BTyCon BTyVar () -> [Symbol]

Reftable (RTProp RTyCon RTyVar Reft)

Methods

isTauto :: RTProp RTyCon RTyVar Reft -> Bool

ppTy :: RTProp RTyCon RTyVar Reft -> Doc -> Doc

top :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft

bot :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft

meet :: RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft -> RTProp RTyCon RTyVar Reft

toReft :: RTProp RTyCon RTyVar Reft -> Reft

ofReft :: Reft -> RTProp RTyCon RTyVar Reft

params :: RTProp RTyCon RTyVar Reft -> [Symbol]

Reftable (RTProp RTyCon RTyVar (UReft Reft))

Methods

isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool

ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc

top :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft)

bot :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft)

meet :: RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft) -> RTProp RTyCon RTyVar (UReft Reft)

toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft

ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft)

params :: RTProp RTyCon RTyVar (UReft Reft) -> [Symbol]

Reftable (RTProp RTyCon RTyVar ())

Methods

isTauto :: RTProp RTyCon RTyVar () -> Bool

ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc

top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar ()

bot :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar ()

meet :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar ()

toReft :: RTProp RTyCon RTyVar () -> Reft

ofReft :: Reft -> RTProp RTyCon RTyVar ()

params :: RTProp RTyCon RTyVar () -> [Symbol]

Reftable (RType BTyCon BTyVar (UReft Reft))

Methods

isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool

ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc

top :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft)

bot :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft)

meet :: RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft) -> RType BTyCon BTyVar (UReft Reft)

toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft

ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft)

params :: RType BTyCon BTyVar (UReft Reft) -> [Symbol]

(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Reftable (RType RTyCon RTyVar r)

Reftable Instances -------------------------------------------------------

Methods

isTauto :: RType RTyCon RTyVar r -> Bool

ppTy :: RType RTyCon RTyVar r -> Doc -> Doc

top :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r

bot :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r

meet :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r

toReft :: RType RTyCon RTyVar r -> Reft

ofReft :: Reft -> RType RTyCon RTyVar r

params :: RType RTyCon RTyVar r -> [Symbol]