Safe Haskell	Safe-Infered

Language.Haskell.Liquid.PredType

Synopsis

Documentation

type PrType = RRType Predicate Source

data TyConP Source

Constructors

TyConP
Fields freeTyVarsTy :: ![RTyVar] freePredTy :: ![PVar RSort]

Instances

Show TyConP
Outputable TyConP

data DataConP Source

Constructors

DataConP
Fields freeTyVars :: ![RTyVar] freePred :: ![PVar RSort] tyArgs :: ![(Symbol, SpecType)] tyRes :: !SpecType

Instances

Show DataConP
Outputable DataConP

dataConTy :: HashMap RTyVar (RType Class RTyCon RTyVar Predicate) -> Type -> RType Class RTyCon RTyVar Predicate Source

dataConPSpecType :: DataConP -> SpecType Source

makeTyConInfo :: [(TyCon, TyConP)] -> HashMap TyCon RTyCon Source

unify :: Maybe PrType -> SpecType -> SpecType Source

replacePreds :: String -> SpecType -> [(RPVar, Ref RReft SpecType)] -> SpecType Source

This is the main function used to substitute an (abstract) predicate with a concrete Ref, of a compound (RPoly) type. The substitution is invoked to obtain the SpecType resulting at predicate application sites in Constraint. The range of the PVar substitutions are fresh or true RefType. That is, there are no further PVar in the target.

exprType :: CoreExpr -> Type Source

predType :: Type Source

replacePredsWithRefs :: (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Refa) -> UReft FReft -> UReft FReft Source

pVartoRConc :: PVar t -> (Symbol, [(a, b, Expr)]) -> Refa Source

toPredType :: Reftable r => PVar (RType Class RTyCon RTyVar a) -> RRType rSource

substParg :: Functor f => (Symbol, Expr) -> f Predicate -> f Predicate Source