A substitution is just a map from names to types.
Moduleth-desugar-1.19Haskell2010
Language.Haskell.TH.Desugar.Subst
Capture-avoiding substitutions on DTypes. (For non–capture-avoiding substitution functions, use Language.Haskell.TH.Desugar.Subst.Capturing instead.)
- 2 types
- 7 values
- Packageth-desugar-1.19
- Exports9
- LanguageHaskell2010
- LicenceBSD-3-Clause
- SourceSubst.hs
Capture-avoiding substitution
6 declarationsCapture-avoiding substitution on DTypes. 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).
Capture-avoiding substitution on DForallTelescopes. 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.
Capture-avoiding substitution on a telescope of DTyVarBndrs. This returns a pair containing the new DSubst as well as a new telescope of DTyVarBndrs, where the names have been renamed to avoid capture and the kinds have been substituted.
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).
Computes the union of two substitutions. Fails if both subsitutions map the same variable to different types.
Matching a type template against a type
2 declarationsmatchTy 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.