--- | Type substitution
---
--- #tvsubst_invariant#
--- The following invariants must hold of a 'TvSubst':
---
--- 1. The in-scope set is needed /only/ to
--- guide the generation of fresh uniques
---
--- 2. In particular, the /kind/ of the type variables in
--- the in-scope set is not relevant
---
--- 3. The substition is only applied ONCE! This is because
--- in general such application will not reached a fixed point.
-data TvSubst
- = TvSubst InScopeSet -- The in-scope type variables
- TvSubstEnv -- The substitution itself
- -- See Note [Apply Once]
- -- and Note [Extending the TvSubstEnv]
-
-{- ----------------------------------------------------------
-
-Note [Apply Once]
-~~~~~~~~~~~~~~~~~
-We use TvSubsts to instantiate things, and we might instantiate
- forall a b. ty
-\with the types
- [a, b], or [b, a].
-So the substition might go [a->b, b->a]. A similar situation arises in Core
-when we find a beta redex like
- (/\ a /\ b -> e) b a
-Then we also end up with a substition that permutes type variables. Other
-variations happen to; for example [a -> (a, b)].
-
- ***************************************************
- *** So a TvSubst must be applied precisely once ***
- ***************************************************
-
-A TvSubst is not idempotent, but, unlike the non-idempotent substitution
-we use during unifications, it must not be repeatedly applied.
-
-Note [Extending the TvSubst]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See #tvsubst_invariant# for the invariants that must hold.
-
-This invariant allows a short-cut when the TvSubstEnv is empty:
-if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) 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 crucial consequences:
-
-* In substTyVarBndr, we need extend the TvSubstEnv
- - if the unique has changed
- - or if the kind has changed
-
-* In substTyVar, we do not need to consult the in-scope set;
- the TvSubstEnv is enough
-
-* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
-
-
--------------------------------------------------------------- -}
-
--- | A substitition of 'Type's for 'TyVar's
-type TvSubstEnv = TyVarEnv Type
- -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
- -- invariant discussed in Note [Apply Once]), and also independently
- -- in the middle of matching, and unification (see Types.Unify)
- -- So you have to look at the context to know if it's idempotent or
- -- apply-once or whatever
-