+ --
+ -- INVARIANT 3: See Note [Extending the Subst]
+\end{code}
+
+Note [Extending the Subst]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+For a core Subst, which binds Ids as well, we make a different choice for Ids
+than we do for TyVars.
+
+For TyVars, see Note [Extending the TvSubst] with Type.TvSubstEnv
+
+For Ids, we have a different invariant
+ The IdSubstEnv is extended *only* when the Unique on an Id changes
+ Otherwise, we just extend the InScopeSet
+
+In consequence:
+
+* In substIdBndr, we extend the IdSubstEnv only when the unique changes
+
+* If the TvSubstEnv and IdSubstEnv are both empty, substExpr does nothing
+ (Note that the above rule for substIdBndr maintains this property. If
+ the incoming envts are both empty, then substituting the type and
+ IdInfo can't change anything.)
+
+* In lookupIdSubst, we *must* look up the Id in the in-scope set, because
+ it may contain non-trivial changes. Example:
+ (/\a. \x:a. ...x...) Int
+ We extend the TvSubstEnv with [a |-> Int]; but x's unique does not change
+ so we only extend the in-scope set. Then we must look up in the in-scope
+ set when we find the occurrence of x.
+
+* The requirement to look up the Id in the in-scope set means that we
+ must NOT take no-op short cut in the case the substitution is empty.
+ We must still look up every Id in the in-scope set.
+
+* (However, we don't need to do so for expressions found in the IdSubst
+ itself, whose range is assumed to be correct wrt the in-scope set.)