opt_univ doesn't track peeled-off type variables
While working on a workaround for #22323, I found out that for a UnivCo :: forall a1 b1. T[a1, b1] ~ forall a2 b2. U[a2, b2]
, GHC.Core.Coercion.Opt.opt_univ
first peels off the outer type variables a1
and a2
, renames a2
to a1
in U
, and then recurses on forall b1. T[a1, b1] ~ forall b2. U[a1, b2]
. However, this then leads to an assertion failure in substTyWith
: since the renaming of b2
to b1
starts with an empty in-scope set, it chockes when it encounters a1
(free in U[a1, b2]
) during substitution.
I tried passing around an InScopeSet
in opt_univ
, but that only works in simple cases when opt_univ
recurses directly to opt_univ
, and not via opt_co4
&c. It feels like the LiftingContext
might be the right place to carry this around, but I don't know enough about where it's otherwise used to really tell.
As a sanity check, replacing the substTyWith
call with substTyWithUnchecked
works as expected, since the final coercion created by opt_univ
wraps the recursive result in the correct ForAllCo
.