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

Functions for lifting Reft-values to Spec-values

uTop :: r -> UReft r 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 #

Applying a solution to a SpecType

Functions for decreasing arguments

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

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

Functions for manipulating Predicates

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 #

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

toType :: ToTypeable r => RRType r -> Type 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 #

Substitutions

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

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

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

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.

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

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

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 #

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

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

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 #

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

Orphan instances

Eq RTyVar Source #

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

Instance details

Methods

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

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

Ord RTyVar Source # 
Instance details

Show RTyVar Source #

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

Instance details

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

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

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

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

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

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

(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

Reftable (RTProp RTyCon RTyVar Reft) Source # 
Instance details

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

Reftable (RTProp BTyCon BTyVar ()) Source # 
Instance details

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

(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

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