diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-05-25 12:23:43 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-05-25 12:33:21 +0100 |
commit | 40d5b9e970149e85f0b5cbc1a795fa36f24a981a (patch) | |
tree | 4f0117f92dce83b08f9db2c96b96e686076ba7dd /compiler | |
parent | c618732ebb234d09abb9f2ef4858d1f96b889a74 (diff) | |
download | haskell-40d5b9e970149e85f0b5cbc1a795fa36f24a981a.tar.gz |
Comments about the substition invariant
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/coreSyn/CoreSubst.hs | 34 | ||||
-rw-r--r-- | compiler/types/TyCoRep.hs | 75 |
2 files changed, 57 insertions, 52 deletions
diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs index ae4458bebe..3d2b4b1a10 100644 --- a/compiler/coreSyn/CoreSubst.hs +++ b/compiler/coreSyn/CoreSubst.hs @@ -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 "CoreSubst#apply_once" +-- 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] diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 2a90a16066..27f28ae429 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -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 |