Commit 685398eb authored by niteria's avatar niteria

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
parent 6f0e41da
......@@ -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)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment