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.