Bogus in-scope set in substitutions

Bartosz reports that substitution isn't working properly for him. He cites this Note in TyCoRep:

-- Note [Generating the in-scope set for a 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))
-- Urk!  This means looking at all the calls to mkOpenTCvSubst....

I think this is an outright bug that has been lurking for ages, and which Bartosz has just managed to tickle.

Things to do:

• We should add an ASSERT to substTy (and similar functions): 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

  That ASSERT could be added to the immediate callers of subst_ty in TyCoRep.

  (Bartosz: if you add that you should find that it trips before the bug you are actually getting.)

• How to fix it properly? The places to look are: everywhere that uses (transitively) one of the mkOpenTCvSubst or zipOpenTCvSubst functions.

  • Many calls to mkOpenTCvSubst produce a substitution that is only applied to closed types; or at least to types whose only free variables are the ones in the domain of the substitution. Example: the call to zipOpenTCvSubst in DataCon.dataConInstSig. These ones will all satisfy the ASSERT.

  • In other cases, we already have the in-scope set in hand. Example: in CoreLint.lintTyApp we find a call to substTyWith. But Lint carries an in-scope set, so it would be easy to pass it to substTyWith.

  • Finally there may be cases where we really have to take the free vars of the type we are substituting into, and add them to the in-scope set.

Doubtless all this applies to substituting in coercions too, and indeed into expressions.