
#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