[commit: ghc] master: Use the correct in-scope set in coercionKind (685398e)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/685398ebc5c8377597714cd8c3e97439d32e3a02/ghc

>---------------------------------------------------------------

commit 685398ebc5c8377597714cd8c3e97439d32e3a02
Author: Bartosz Nitka <niteria at gmail.com>
Date:   Mon Mar 21 11:11:26 2016 -0700

    Use the correct in-scope set in coercionKind
    
    The free vars of `ty2` need to be in scope to satisfy the substitution
    invariant.
    As far as I can tell we don't have the free vars of `ty2` when
    substituting, so unfortunately we have to compute them.
    
    Test Plan: ./validate
    
    Reviewers: austin, bgamari, simonpj, goldfire
    
    Subscribers: thomie, simonmar
    
    Differential Revision: https://phabricator.haskell.org/D2024
    
    GHC Trac Issues: #11371


>---------------------------------------------------------------

685398ebc5c8377597714cd8c3e97439d32e3a02
 compiler/types/Coercion.hs | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index e8d1d6c..a2b93bd 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -1717,7 +1717,12 @@ coercionKind co = go co
       = let Pair _ k2          = go k_co
             tv2                = setTyVarKind tv1 k2
             Pair ty1 ty2       = go co
-            ty2' = substTyWithUnchecked [tv1] [TyVarTy tv2 `mk_cast_ty` mkSymCo k_co] ty2 in
+            subst = zipTvSubst [tv1] [TyVarTy tv2 `mk_cast_ty` mkSymCo k_co]
+            ty2' = substTyAddInScope subst ty2 in
+            -- We need free vars of ty2 in scope to satisfy the invariant
+            -- from Note [The substitution invariant]
+            -- This is doing repeated substitutions and probably doesn't
+            -- need to, see #11735
         mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2'
     go (CoVarCo cv)         = toPair $ coVarTypes cv
     go (AxiomInstCo ax ind cos)
@@ -1792,7 +1797,12 @@ coercionKindRole = go
       = let Pair _ k2          = coercionKind k_co
             tv2                = setTyVarKind tv1 k2
             (Pair ty1 ty2, r)  = go co
-            ty2' = substTyWithUnchecked [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo k_co] ty2 in
+            subst = zipTvSubst [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo k_co]
+            ty2' = substTyAddInScope subst ty2 in
+            -- We need free vars of ty2 in scope to satisfy the invariant
+            -- from Note [The substitution invariant]
+            -- This is doing repeated substitutions and probably doesn't
+            -- need to, see #11735
         (mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2', r)
     go (CoVarCo cv) = (toPair $ coVarTypes cv, coVarRole cv)
     go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)