Copyright | (C) 2024 Ryan Scott |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Language.Haskell.TH.Desugar.Subst.Capturing
Description
Substitutions on DType
s that do not avoid capture. (For capture-avoiding
substitution functions, use Language.Haskell.TH.Desugar.Subst instead.)
Synopsis
- type DSubst = Map Name DType
- substTy :: DSubst -> DType -> DType
- substForallTelescope :: DSubst -> DForallTelescope -> (DSubst, DForallTelescope)
- substTyVarBndrs :: DSubst -> [DTyVarBndr flag] -> (DSubst, [DTyVarBndr flag])
- substTyVarBndr :: DSubst -> DTyVarBndr flag -> (DSubst, DTyVarBndr flag)
- unionSubsts :: DSubst -> DSubst -> Maybe DSubst
- unionMaybeSubsts :: [Maybe DSubst] -> Maybe DSubst
- data IgnoreKinds
- matchTy :: IgnoreKinds -> DType -> DType -> Maybe DSubst
Documentation
Non–capture-avoiding substitution
substTy :: DSubst -> DType -> DType Source #
Non–capture-avoiding substitution on DType
s. Unlike the substTy
function in Language.Haskell.TH.Desugar.Subst, this substTy
function is
pure, as it never needs to create fresh names.
substForallTelescope :: DSubst -> DForallTelescope -> (DSubst, DForallTelescope) Source #
Non–capture-avoiding substitution on DForallTelescope
s. This returns a
pair containing the new DSubst
as well as a new DForallTelescope
value,
where the kinds have been substituted.
substTyVarBndrs :: DSubst -> [DTyVarBndr flag] -> (DSubst, [DTyVarBndr flag]) Source #
Non–capture-avoiding substitution on a telescope of DTyVarBndr
s. This
returns a pair containing the new DSubst
as well as a new telescope of
DTyVarBndr
s, where the kinds have been substituted.
substTyVarBndr :: DSubst -> DTyVarBndr flag -> (DSubst, DTyVarBndr flag) Source #
Non–capture-avoiding substitution on a DTyVarBndr
. This updates the
DSubst
to remove the DTyVarBndr
name from the domain (as that name is now
bound by the DTyVarBndr
) and applies the substitution to the kind of the
DTyVarBndr
.
unionSubsts :: DSubst -> DSubst -> Maybe DSubst Source #
Computes the union of two substitutions. Fails if both subsitutions map the same variable to different types.
Matching a type template against a type
matchTy :: IgnoreKinds -> DType -> DType -> Maybe DSubst Source #
matchTy ign tmpl targ
matches a type template tmpl
against a type
target targ
. This returns a Map from names of type variables in the
type template to types if the types indeed match up, or Nothing
otherwise.
In the Just
case, it is guaranteed that every type variable mentioned
in the template is mapped by the returned substitution.
The first argument ign
tells matchTy
whether to ignore kind signatures
in the template. A kind signature in the template might mean that a type
variable has a more restrictive kind than otherwise possible, and that
mapping that type variable to a type of a different kind could be disastrous.
So, if we don't ignore kind signatures, this function returns Nothing
if
the template has a signature anywhere. If we do ignore kind signatures, it's
possible the returned map will be ill-kinded. Use at your own risk.