Copyright | (C) 2018 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Language.Haskell.TH.Desugar.Subst
Description
Capture-avoiding substitutions on DType
s. (For non–capture-avoiding
substitution functions, use Language.Haskell.TH.Desugar.Subst.Capturing
instead.)
Synopsis
- type DSubst = Map Name DType
- substTy :: Quasi q => DSubst -> DType -> q DType
- substForallTelescope :: Quasi q => DSubst -> DForallTelescope -> q (DSubst, DForallTelescope)
- substTyVarBndrs :: Quasi q => DSubst -> [DTyVarBndr flag] -> q (DSubst, [DTyVarBndr flag])
- substTyVarBndr :: Quasi q => DSubst -> DTyVarBndr flag -> q (DSubst, DTyVarBndr flag)
- unionSubsts :: DSubst -> DSubst -> Maybe DSubst
- unionMaybeSubsts :: [Maybe DSubst] -> Maybe DSubst
- data IgnoreKinds
- matchTy :: IgnoreKinds -> DType -> DType -> Maybe DSubst
Documentation
Capture-avoiding substitution
substTy :: Quasi q => DSubst -> DType -> q DType Source #
Capture-avoiding substitution on DType
s. This function requires a Quasi
constraint because it may need to create fresh names in order to avoid
capture when substituting into a forall
type (see substTyVarBndr
).
substForallTelescope :: Quasi q => DSubst -> DForallTelescope -> q (DSubst, DForallTelescope) Source #
Capture-avoiding substitution on DForallTelescope
s. This returns a pair
containing the new DSubst
as well as a new DForallTelescope
value, where
the names have been renamed to avoid capture and the kinds have been
substituted.
substTyVarBndrs :: Quasi q => DSubst -> [DTyVarBndr flag] -> q (DSubst, [DTyVarBndr flag]) Source #
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 names have been renamed to avoid capture and the
kinds have been substituted.
substTyVarBndr :: Quasi q => DSubst -> DTyVarBndr flag -> q (DSubst, DTyVarBndr flag) Source #
Capture-avoiding substitution on a DTyVarBndr
. This uses the Quasi
constraint to create a new, fresh name (based on the name of the supplied
DTyVarBndr
), update the DSubst
to map from the old name to the new name,
and this also returns a DTyVarBndr
containing the new name and the kind of
the supplied DTyVarBndr
(with the substitution applied).
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.