| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Cryptol.TypeCheck.Subst.Type
Description
Most of this module is re-exported by Cryptol.TypeCheck.Subst, so you probably want to import that instead of this.
The exception being, if you want to substitute types without performing
simplification afterwards, then you should use apSubstNoSimp from this
module. It is in this module so that you can use it from places like the
typeclass solver itself, to avoid a module import cycle (since the regular
apSubst has to import the class solver to do the
substitution).
Synopsis
- data Subst = S {
- suFreeMap :: !(IntMap (TVar, Type))
- suBoundMap :: !(IntMap (TVar, Type))
- suDefaulting :: !Bool
- emptySubst :: Subst
- data SubstError
- singleSubst :: TVar -> Type -> Either SubstError Subst
- singleTParamSubst :: TParam -> Type -> Subst
- uncheckedSingleSubst :: TVar -> Type -> Subst
- defaultingSubst :: Subst -> Subst
- listSubst :: [(TVar, Type)] -> Subst
- listParamSubst :: [(TParam, Type)] -> Subst
- isEmptySubst :: Subst -> Bool
- substBinds :: Subst -> Set TVar
- substToList :: Subst -> [(TVar, Type)]
- mergeDistinctSubst :: [Subst] -> Subst
- apSubstMaybe' :: (Prop -> Prop) -> Subst -> Type -> Maybe Type
- applySubstToVar' :: (Subst -> Type -> Maybe Type) -> Subst -> TVar -> Maybe Type
- apSubstNoSimp :: Subst -> Type -> Type
Documentation
A Subst value represents a substitution that maps each TVar
to a Type.
Invariant 1: If there is a mapping from TVFree _ _ tps _ to a
type t, then t must not mention (directly or indirectly) any
type parameter that is not in tps. In particular, if t contains
a variable TVFree _ _ tps2 _, then tps2 must be a subset of
tps. This ensures that applying the substitution will not permit
any type parameter to escape from its scope.
Invariant 2: The substitution must be idempotent, in that applying
a substitution to any Type in the map should leave that Type
unchanged. In other words, Type values in the range of a Subst
should not mention any TVar in the domain of the Subst. In
particular, this implies that a substitution must not contain any
recursive variable mappings.
Invariant 3: The substitution must be kind correct: Each TVar in
the substitution must map to a Type of the same kind.
Constructors
| S | |
Fields
| |
emptySubst :: Subst Source #
data SubstError Source #
Reasons to reject a single-variable substitution.
Constructors
| SubstRecursive |
|
| SubstEscaped [TParam] |
|
| SubstKindMismatch Kind Kind |
|
singleSubst :: TVar -> Type -> Either SubstError Subst Source #
defaultingSubst :: Subst -> Subst Source #
A defaulting substitution maps all otherwise-unmapped free
variables to a kind-appropriate default type (Bit for value types
and 0 for numeric types).
listSubst :: [(TVar, Type)] -> Subst Source #
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.
listParamSubst :: [(TParam, Type)] -> Subst Source #
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 Source #
mergeDistinctSubst :: [Subst] -> Subst Source #
apSubstMaybe' :: (Prop -> Prop) -> Subst -> Type -> Maybe Type Source #
Apply a substitution. Returns Nothing if nothing changed.
The Prop -> Prop function is how to simplify the result if it is a
predicate.
apSubstNoSimp :: Subst -> Type -> Type Source #
Apply a substitution without simplifying the result when it is a predicate.
This is used by the typeclass solver itself, if it needs to perform
substitution; e.g., when solving derived instances for nominal types. Some
code asks the typeclass solver to do only a single simplification step; if it
called the regular apSubst which simplifies
recursively after substitution, then it would do many simplification steps
instead of one, resulting in worse error messages. Not doing simplification
also allows us to avoid a module dependency cycle.