Type substitution

The following invariants must hold:

1. The InScopeSet is needed only to guide the generation of fresh uniques
2. In particular, the kind of the type variables in the InScopeSet is not relevant.
3. The substitution is only applied once

Note [Apply Once]

We might instantiate forall a b. ty with the types [a, b] or [b, a]. So the substitution might go like [a -> b, b -> a]. A similar situation arises in terms when we find a redex like (a -> b -> e) b a. Then we also end up with a substitution that permutes variables. Other variations happen to; for example [a -> (a,b)].

SO A TvSubst MUST BE APPLIED PRECISELY ONCE, OR THINGS MIGHT LOOP

Note [The substitution invariant]

When calling (substTy subst ty) it should be the case that the InScopeSet is a superset of both:

• The free variables of the range of the substitution
• The free variables of ty minus the domain of the substitution

A substitution of Types for Vars

Note [Extending the TvSubstEnv] See TvSubst for the invariants that must hold

This invariant allows a short-cut when the subst env is empty: if the TvSubstEnv is empty, i.e. nullVarEnv TvSubstEnv holds, then (substTy subst ty) does nothing.

For example, consider:

(a -> b(a ~ Int) -> ... b ...) Int

We substitute Int for a. The Unique of b does not change, but nevertheless we add b to the TvSubstEnv because b's kind does change

This invariant has several consequences:

• In substTyVarBndr, we extend TvSubstEnv if the unique has changed, or if the kind has changed
• In substTyVar, we do not need to consult the InScopeSet; the TvSubstEnv is enough
• In substTy, we can short-circuit when TvSubstEnv is empty

Extend the substitution environment with a new Var substitution

Extend the substitution environment with a list of Var substitutions

Substitute within a Type

The substitution has to satisfy the invariant described in TvSubsts Note [The substitution environment]

Type substitution, see zipTvSubst

Works only if the domain of the substitution is superset of the type being substituted into

Substitute within a Var. See substTy.

Safely substitute a type variable in a list of existentials. This function will account for cases where existentials shadow each other.

Safely substitute type variables in a list of existentials. This function will account for cases where existentials shadow each other.

A substitution environment containing containing both Var and Var substitutions.

Some invariants apply to how you use the substitution:

1. The InScopeSet contains at least those Vars and Vars that will be in scope after applying the substitution to a term. Precisely, the in-scope set must be a superset of the free variables of the substitution range that might possibly clash with locally-bound variables in the thing being substituted in.
2. You may only apply the substitution once. See TvSubst

There are various ways of setting up the in-scope set such that the first of of these invariants holds:

• Arrange that the in-scope set really is all the things in scope
• Arrange that it's the free vars of the range of the substitution
• Make it empty, if you know that all the free variables of the substitution are fresh, and hence can´t possibly clash

An empty substitution, starting the variables currently in scope

Create a type substitution

Add an Var to the in-scope set: as a side effect, remove any existing substitutions for it.

Add Vars to the in-scope set. See also extendInScopeId

Extend the substitution environment with a new Var substitution

Extend the substitution environment with a list of Var substitutions

Extend the substitution environment with a list of global Var substitutions

Substitute within a Term

Substitute within a Term. Just return original term if given substitution is Nothing.

Like substTm, but doesn't account for shadowing or free variable capture.

An example of shadowing: in (x, x -> x) with a substitution x |-> 5 unsafeSubstTm will yield (5, x -> 5), whereas a safe substitution would yield (5, x -> x).

An example of free variable capture: in x -> y and a substitution y |-> f x, unsafeSubstTm will yield x -> f x, whereas a safe substitution would yield x' -> f x.

You should therefore only use this function if:

1. No binder in the term binds variables in the domain of the local substitution.
2. No binder in the term has the same unique as a local, free variable of any replacement term in the range of either substitution.

Both conditions hold if the term is deshadowed (see deShadowTerm) with respect to an in-scope set that contains the domains of the substitutions and the free variables of the replacement terms.

Note that global substituations are always safe. They never have local free variables and cannot be introduced through a binder. I.e., neither rule 1 nor 2 applies.

Substitute within a case-alternative

Ensure that non of the binders in an expression shadow each-other, nor conflict with he in-scope set

Ensure that non of the binders in an alternative shadow each-other, nor conflict with the in-scope set

A much stronger variant of deShadowTerm that ensures that all bound variables are unique.

Also returns an extended InScopeSet additionally containing the (renamed) unique bound variables of the term.

Ensure that non of the let-bindings of a let-expression shadow w.r.t the in-scope set

Alpha equality for types

Alpha equality for terms

Alpha comparison for terms

Alpha equality for ticks

Alpha comparison for ticks

Alpha equality for ticks, under the binders enclosing them. See acmpTickInfoLevels.

Alpha comparison for ticks, under the binders enclosing them.

The Type in NameMod and the Term in Attributes live in the scope enclosing the tick, so they are compared under the same binders as the term the tick is attached to. TickInfos are compared with leftmost_smallest, which treats all unhelpful spans alike, so it is coarser than Eq TickInfo.

Structural equality on Term

Structural equality on Type