liquidhaskell-0.8.10.2: Liquid Types for Haskell
Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Types.RefType

Description

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

Synopsis

Documentation

data TyConMap Source #

Information about Type Constructors

Instances

Instances details
Qualify TyConMap Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Methods

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

Functions for lifting Reft-values to Spec-values

uTop :: r -> UReft r Source #

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

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

Various functions for converting vanilla Reft to Spec

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

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

uPVar :: PVar t -> UsedPVar Source #

Applying a solution to a SpecType

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

Functions for decreasing arguments

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

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

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

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

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

Functions for manipulating Predicates

pdVar :: PVar t -> Predicate Source #

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

class FreeVar a v Source #

Minimal complete definition

freeVars

Instances

Instances details
FreeVar RTyCon RTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: RTyCon -> [RTyVar]

FreeVar BTyCon BTyVar Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

freeVars :: BTyCon -> [BTyVar]

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

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

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

tyConName :: TyCon -> Symbol Source #

Quantifying RTypes

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

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

RType constructors

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

toType :: ToTypeable r => RRType r -> Type Source #

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

bTyVar :: Symbol -> BTyVar Source #

rTyVar :: TyVar -> RTyVar Source #

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

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

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

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

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

symbolRTyVar :: Symbol -> RTyVar Source #

bareRTyVar :: BTyVar -> RTyVar Source #

tyConBTyCon :: TyCon -> BTyCon Source #

pdVarReft :: PVar t -> UReft Reft Source #

Substitutions

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

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

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

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

subsTyVar_meet :: (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 Source #

subsTyVar_meet' :: (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 Source #

subsTyVar_nomeet :: (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 Source #

subsTyVars_nomeet :: (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 Source #

subsTyVars_meet :: (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 Source #

Destructors

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

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

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

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

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

isSizeable :: HashSet TyCon -> TyCon -> Bool Source #

famInstTyConType :: TyCon -> Maybe Type Source #

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

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

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

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

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

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

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

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

typeSort :: TCEmb TyCon -> Type -> Sort Source #

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

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

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

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

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

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

isBaseTy :: Type -> Bool Source #

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

isValKind :: Kind -> Bool Source #

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

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

tyVarsPosition :: RType RTyCon tv r -> Positions tv Source #

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

Constructors

Pos 

Fields

Instances

Instances details
Semigroup (Positions a) Source # 
Instance details

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 #

Monoid (Positions a) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.RefType

Methods

mempty :: Positions a #

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

mconcat :: [Positions a] -> Positions a #

isNumeric :: TCEmb TyCon -> RTyCon -> Bool Source #

Orphan instances

Eq RTyVar Source #

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

Instance details

Methods

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

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

Ord RTyVar Source # 
Instance details

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 #

Show RTyVar Source #

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

Instance details

Methods

showsPrec :: Int -> RTyVar -> ShowS #

show :: RTyVar -> String #

showList :: [RTyVar] -> ShowS #

Hashable RTyCon Source # 
Instance details

Methods

hashWithSalt :: Int -> RTyCon -> Int #

hash :: RTyCon -> Int #

Hashable RTyVar Source # 
Instance details

Methods

hashWithSalt :: Int -> RTyVar -> Int #

hash :: RTyVar -> Int #

Expression Var Source #

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

Instance details

Methods

expr :: Var -> Expr #

Fixpoint String Source # 
Instance details

Methods

toFix :: String -> Doc #

simplify :: String -> String #

Fixpoint Class Source # 
Instance details

Methods

toFix :: Class -> Doc #

simplify :: Class -> Class #

PPrint DataCtor Source # 
Instance details

Methods

pprintTidy :: Tidy -> DataCtor -> Doc #

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

PPrint DataDecl Source # 
Instance details

Methods

pprintTidy :: Tidy -> DataDecl -> Doc #

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

SubsTy tv RSort Predicate Source # 
Instance details

Methods

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

SubsTy tv ty Sort => SubsTy tv ty Expr Source # 
Instance details

Methods

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

SubsTy tv ty Expr => SubsTy tv ty Reft Source # 
Instance details

Methods

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

SubsTy tv ty Symbol Source # 
Instance details

Methods

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

SubsTy tv ty () Source # 
Instance details

Methods

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

SubsTy TyVar Type SpecType Source # 
Instance details

Methods

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

SubsTy Symbol RSort Sort Source # 
Instance details

Methods

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

SubsTy RTyVar RSort Sort Source # 
Instance details

Methods

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

SubsTy RTyVar RSort SpecType Source # 
Instance details

Methods

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

SubsTy RTyVar RSort PrType Source # 
Instance details

Methods

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

SubsTy RTyVar RSort RSort Source # 
Instance details

Methods

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

SubsTy RTyVar RSort RTyCon Source # 
Instance details

Methods

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

SubsTy RTyVar RTyVar SpecType Source # 
Instance details

Methods

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

SubsTy BTyVar BSort BSort Source # 
Instance details

Methods

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

SubsTy BTyVar BSort BTyCon Source # 
Instance details

Methods

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

SubsTy tv ty r => SubsTy tv ty (UReft r) Source # 
Instance details

Methods

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

SubsTy tv ty ty => SubsTy tv ty (PVar ty) Source # 
Instance details

Methods

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

SubsTy tv ty ty => SubsTy tv ty (PVKind ty) Source # 
Instance details

Methods

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

SubsTy Symbol Symbol (BRType r) Source # 
Instance details

Methods

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

(SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b) Source # 
Instance details

Methods

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

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r)) Source # 
Instance details

Methods

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

SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) Source # 
Instance details

Methods

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

SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar Source # 
Instance details

Methods

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

SubsTy BTyVar (RType c BTyVar ()) BTyVar Source # 
Instance details

Methods

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

SubsTy BTyVar (RType BTyCon BTyVar ()) Sort Source # 
Instance details

Methods

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

SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) Source # 
Instance details

Methods

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

SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) Source # 
Instance details

Methods

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

PPrint (UReft r) => Show (UReft r) Source # 
Instance details

Methods

showsPrec :: Int -> UReft r -> ShowS #

show :: UReft r -> String #

showList :: [UReft r] -> ShowS #

Subable (RRProp Reft) Source #

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

Instance details

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) Source #

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

Instance details

Methods

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

show :: RTAlias tv ty -> String #

showList :: [RTAlias tv ty] -> ShowS #

(Eq c, Eq tv, Hashable tv, PPrint tv, TyConable c, PPrint c, Reftable (RTProp c tv ())) => Eq (RType c tv ()) Source # 
Instance details

Methods

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

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

PPrint (RTProp c tv r) => Show (RTProp c tv r) Source # 
Instance details

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

Methods

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

show :: RType c tv r -> String #

showList :: [RType c tv r] -> 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 ()))) => Semigroup (RTProp c tv r) Source # 
Instance details

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

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 #

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

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

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 #

Reftable (RTProp RTyCon RTyVar ()) Source # 
Instance details

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 (RTProp RTyCon RTyVar Reft) Source # 
Instance details

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

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 BTyCon BTyVar ()) Source # 
Instance details

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 BTyCon BTyVar (UReft Reft)) Source # 
Instance details

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] #

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

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

Instance details

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] #

Reftable (RType BTyCon BTyVar (UReft Reft)) Source # 
Instance details

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] #