th-desugar-1.18: Functions to desugar Template Haskell
Copyright(C) 2024 Ryan Scott
LicenseBSD-style (see LICENSE)
MaintainerRyan Scott
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Language.Haskell.TH.Desugar.Subst.Capturing

Description

Substitutions on DTypes that do not avoid capture. (For capture-avoiding substitution functions, use Language.Haskell.TH.Desugar.Subst instead.)

Synopsis

Documentation

type DSubst = Map Name DType Source #

A substitution is just a map from names to types.

Non–capture-avoiding substitution

substTy :: DSubst -> DType -> DType Source #

Non–capture-avoiding substitution on DTypes. 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 DForallTelescopes. 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 DTyVarBndrs. This returns a pair containing the new DSubst as well as a new telescope of DTyVarBndrs, 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

data IgnoreKinds Source #

Ignore kind annotations in matchTy?

Constructors

YesIgnore 
NoIgnore 

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.