Note [Optimising ForAllCo]
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
- ForAllCo GHC.Core.TyCo.Rep
Referenced by 1
- GHC.Core.Coercion.Opt call site