Use the correct in-scope set in coercionKind
authorBartosz Nitka <niteria@gmail.com>
Mon, 21 Mar 2016 18:11:26 +0000 (11:11 -0700)
committerBartosz Nitka <niteria@gmail.com>
Mon, 21 Mar 2016 22:17:06 +0000 (15:17 -0700)
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

compiler/types/Coercion.hs

index e8d1d6c..a2b93bd 100644 (file)
@@ -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)