Language.Haskell.TH.Desugar.Subst

Capture-avoiding substitutions on DTypes

Documentation

type DSubst = Map Name DType

A substitution is just a map from names to types

Capture-avoiding substitution

substTy :: Quasi q => DSubst -> DType -> q DType

Capture-avoiding substitution on types

substForallTelescope :: Quasi q => DSubst -> DForallTelescope -> q (DSubst, DForallTelescope)

substTyVarBndrs :: Quasi q => DSubst -> [DTyVarBndr flag] -> q (DSubst, [DTyVarBndr flag])

unionSubsts :: DSubst -> DSubst -> Maybe DSubst

Computes the union of two substitutions. Fails if both subsitutions map the same variable to different types.

unionMaybeSubsts :: [Maybe DSubst] -> Maybe DSubst

Matching a type template against a type

data IgnoreKinds

Ignore kind annotations in matchTy?

Constructors

YesIgnore

NoIgnore

matchTy :: IgnoreKinds -> DType -> DType -> Maybe DSubst

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.