Note [Optimising ForAllCo]

GHC/Core/Coercion/Opt.hs:1404 compiler

If sym=NotSwapped, optimising ForAllCo is relatively easy:
   opt env (ForAllCo tcv kco bodyco)
     = ForAllCo tcv' (opt env kco) (opt env' bodyco)
     where
       (env', tcv') = substBndr env tcv

Just apply the substitution to the kind of the binder, deal with
shadowing etc, and recurse.  Remember in (ForAllCo tcv kco bodyco)
    varKind tcv = coercionLKind kco

But if sym=Swapped, things are trickier.  Here is an identity that helps:
   Sym (ForAllCo (tv:k1) (kco:k1~k2) bodyco)
   = ForAllCo (tv:k2) (Sym kco : k2~k1)
              (Sym (bodyco[tv:->tv:k2 |> Sym kco]))

* We re-type tv:k1 to become tv:k2.
* We push Sym into kco
* We push Sym into bodyco
* BUT we must /also/ remember to replace all occurrences of
      of tv:k1 in bodyco by (tv:k2 |> Sym kco)
  This mirrors what happens in the typing rule for ForAllCo
  See Note [ForAllCo] in GHC.Core.TyCo.Rep

References 1

Referenced by 1