[GHC] #11371: Bogus in-scope set in substitutions

[GHC]

#11371: Bogus in-scope set in substitutions
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.2.1
          Component:  Compiler       |           Version:  7.10.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Bartosz [https://mail.haskell.org/pipermail/ghc-
 devs/2016-January/010892.html 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**
   * **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[[BR]][[BR]]
   * 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`.[[BR]][[BR]]
   * 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11371>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler