Commit 40d5b9e9 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Comments about the substition invariant

parent c618732e
......@@ -79,19 +79,9 @@ import Data.List
--
-- Some invariants apply to how you use the substitution:
--
-- 1. #in_scope_invariant# The in-scope set contains at least those 'Id's and 'TyVar's that will be in scope /after/
-- applying the substitution to a term. Precisely, the in-scope set must be a superset of the free vars of the
-- substitution range that might possibly clash with locally-bound variables in the thing being substituted in.
-- 1. Note [The substitution invariant] in TyCoRep
--
-- 2. #apply_once# You may apply the substitution only /once/
--
-- There are various ways of setting up the in-scope set such that the first of these invariants hold:
--
-- * 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 vars of the substitution are fresh, and hence can't possibly clash
-- 2. Note [Substitutions apply only once] in TyCoRep
data Subst
= Subst InScopeSet -- Variables in in scope (both Ids and TyVars) /after/
-- applying the substitution
......@@ -99,7 +89,7 @@ data Subst
TvSubstEnv -- Substitution from TyVars to Types
CvSubstEnv -- Substitution from CoVars to Coercions
-- INVARIANT 1: See #in_scope_invariant#
-- INVARIANT 1: See TyCORep Note [The substitution invariant]
-- This is what lets us deal with name capture properly
-- It's a hard invariant to check...
--
......@@ -181,7 +171,7 @@ mkEmptySubst in_scope = Subst in_scope emptyVarEnv emptyVarEnv emptyVarEnv
mkSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst
mkSubst in_scope tvs cvs ids = Subst in_scope ids tvs cvs
-- | Find the in-scope set: see "CoreSubst#in_scope_invariant"
-- | Find the in-scope set: see TyCORep Note [The substitution invariant]
substInScope :: Subst -> InScopeSet
substInScope (Subst in_scope _ _ _) = in_scope
......@@ -191,7 +181,8 @@ zapSubstEnv :: Subst -> Subst
zapSubstEnv (Subst in_scope _ _ _) = Subst in_scope emptyVarEnv emptyVarEnv emptyVarEnv
-- | Add a substitution for an 'Id' to the 'Subst': you must ensure that the in-scope set is
-- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
-- such that TyCORep Note [The substitution invariant]
-- holds after extending the substitution like this
extendIdSubst :: Subst -> Id -> CoreExpr -> Subst
-- ToDo: add an ASSERT that fvs(subst-result) is already in the in-scope set
extendIdSubst (Subst in_scope ids tvs cvs) v r
......@@ -207,8 +198,8 @@ extendIdSubstList (Subst in_scope ids tvs cvs) prs
-- | Add a substitution for a 'TyVar' to the 'Subst'
-- The 'TyVar' *must* be a real TyVar, and not a CoVar
-- You must ensure that the in-scope set is such that
-- the "CoreSubst#in_scope_invariant" is true after extending
-- the substitution like this.
-- TyCORep Note [The substitution invariant] holds
-- after extending the substitution like this.
extendTvSubst :: Subst -> TyVar -> Type -> Subst
extendTvSubst (Subst in_scope ids tvs cvs) tv ty
= ASSERT( isTyVar tv )
......@@ -221,8 +212,10 @@ extendTvSubstList subst vrs
where
extend subst (v, r) = extendTvSubst subst v r
-- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst': you must ensure that the in-scope set is
-- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
-- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst':
-- you must ensure that the in-scope set satisfies
-- TyCORep Note [The substitution invariant]
-- after extending the substitution like this
extendCvSubst :: Subst -> CoVar -> Coercion -> Subst
extendCvSubst (Subst in_scope ids tvs cvs) v r
= ASSERT( isCoVar v )
......@@ -345,7 +338,8 @@ instance Outputable Subst where
-}
-- | Apply a substitution to an entire 'CoreExpr'. Remember, you may only
-- apply the substitution /once/:
-- see Note [Substitutions apply only once] in TyCoRep
--
-- Do *not* attempt to short-cut in the case of an empty substitution!
-- See Note [Extending the Subst]
......
......@@ -1808,7 +1808,7 @@ data TCvSubst
= TCvSubst InScopeSet -- The in-scope type and kind variables
TvSubstEnv -- Substitutes both type and kind variables
CvSubstEnv -- Substitutes coercion variables
-- See Note [Apply Once]
-- See Note [Substitutions apply only once]
-- and Note [Extending the TvSubstEnv]
-- and Note [Substituting types and coercions]
-- and Note [The substitution invariant]
......@@ -1816,21 +1816,51 @@ data TCvSubst
-- | A substitution of 'Type's for 'TyVar's
-- and 'Kind's for 'KindVar's
type TvSubstEnv = TyVarEnv Type
-- A TvSubstEnv is used both inside a TCvSubst (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
-- NB: A TvSubstEnv is used
-- both inside a TCvSubst (with the apply-once invariant
-- discussed in Note [Substitutions apply only 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
-- | A substitution of 'Coercion's for 'CoVar's
type CvSubstEnv = CoVarEnv Coercion
{-
Note [Apply Once]
~~~~~~~~~~~~~~~~~
{- Note [The substitution invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When calling (substTy subst ty) it should be the case that
the in-scope set in the substitution is a superset of both:
(SIa) The free vars of the range of the substitution
(SIb) The free vars of ty minus the domain of the substitution
The same rules apply to other substitutions (notably CoreSubst.Subst)
* Reason for (SIa). Consider
substTy [a :-> Maybe b] (forall b. b->a)
we must rename the forall b, to get
forall b2. b2 -> Maybe b
Making 'b' part of the in-scope set forces this renaming to
take place.
* Reason for (SIb). Consider
substTy [a :-> Maybe b] (forall b. (a,b,x))
Then if we use the in-scope set {b}, satisfying (SIa), there is
a danger we will rename the forall'd variable to 'x' by mistake,
getting this:
forall x. (List b, x, x)
Breaking (SIb) caused the bug from #11371.
Note: if the free vars of the range of the substitution are freshly created,
then the problems of (SIa) can't happen, and so it would be sound to
ignore (SIa).
Note [Substitutions apply only once]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We use TCvSubsts to instantiate things, and we might instantiate
forall a b. ty
\with the types
with the types
[a, b], or [b, a].
So the substitution might go [a->b, b->a]. A similar situation arises in Core
when we find a beta redex like
......@@ -1838,9 +1868,9 @@ when we find a beta redex like
Then we also end up with a substitution that permutes type variables. Other
variations happen to; for example [a -> (a, b)].
****************************************************
*** So a TCvSubst must be applied precisely once ***
****************************************************
********************************************************
*** So a substitution must be applied precisely once ***
********************************************************
A TCvSubst is not idempotent, but, unlike the non-idempotent substitution
we use during unifications, it must not be repeatedly applied.
......@@ -1883,25 +1913,6 @@ Note that the TvSubstEnv should *never* map a CoVar (built with the Id
constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore,
the range of the TvSubstEnv should *never* include a type headed with
CoercionTy.
Note [The substitution invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When calling (substTy subst ty) it should be the case that
the in-scope set in the substitution is a superset of both:
* The free vars of the range of the substitution
* The free vars of ty minus the domain of the substitution
If we want to substitute [a -> ty1, b -> ty2] I used to
think it was enough to generate an in-scope set that includes
fv(ty1,ty2). But that's not enough; we really should also take the
free vars of the type we are substituting into! Example:
(forall b. (a,b,x)) [a -> List b]
Then if we use the in-scope set {b}, there is a danger we will rename
the forall'd variable to 'x' by mistake, getting this:
(forall x. (List b, x, x))
Breaking this invariant caused the bug from #11371.
-}
emptyTvSubstEnv :: TvSubstEnv
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment