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

[GHC]

#11371: Bogus in-scope set in substitutions
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  niteria
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11360            |  Differential Rev(s):  phab:D1792
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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.

New description:

 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 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[[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#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler