Cryptol.TypeCheck.Subst

Documentation

data Subst

Constructors

S

Fields

suMap :: Map TVar Type

suDefaulting :: !Bool

Instances

Show Subst

PP Subst

DebugLog Subst

PP (WithNames Subst)

emptySubst :: Subst

singleSubst :: TVar -> Type -> Subst

(@@) :: Subst -> Subst -> Subst

defaultingSubst :: Subst -> Subst

listSubst :: [(TVar, Type)] -> Subst

Makes a substitution out of a list. WARNING: We do not validate the list in any way, so the caller should ensure that we end up with a valid (e.g., idempotent) substitution.

isEmptySubst :: Subst -> Bool

substToList :: Subst -> Maybe [(TVar, Type)]

class FVS t where

Methods

fvs :: t -> Set TVar

Instances

FVS Type

FVS Schema

FVS Error

FVS Warning

FVS DelayedCt

FVS Goal

FVS a => FVS [a]

(FVS a, FVS b) => FVS (a, b)

apSubstMaybe :: Subst -> Type -> Maybe Type

Apply a substitution. Returns Nothing if nothing changed.

class TVars t where

Methods

apSubst

Arguments

:: Subst

-> t

-> t

replaces free vars

Instances

TVars DeclDef

TVars Decl

TVars DeclGroup

TVars Match

TVars Expr

TVars Type

TVars Schema

WARNING: This instance assumes that the quantified variables in the types in the substitution will not get captured by the quantified variables. This is reasonable because there should be no shadowing of quantified variables but, just in case, we make a sanity check and panic if somehow capture did occur.

TVars Module

TVars ConstraintSource

TVars Error

TVars Warning

TVars DelayedCt

TVars HasGoal

TVars Goal

TVars Goals

TVars t => TVars [t]

TVars t => TVars (Maybe t)

TVars a => TVars (TypeMap a)

(TVars s, TVars t) => TVars (s, t)

(Functor m, TVars a) => TVars (List m a)

defaultFreeVar :: TVar -> Type

Pick types for unconstrained unification variables.

apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a

Apply the substitution to the keys of a type map.