Treatment of local CoVarCo in coercion optimization is almost surely wrong
Currently, we have
opt_co4 env sym rep r (CoVarCo cv)
| Just co <- lookupCoVar (lcTCvSubst env) cv
= opt_co4_wrap (zapLiftingContext env) sym rep r co
...
opt_co4 env sym rep r (InstCo co1 arg)
-- forall over coercion...
| Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1
, CoercionTy h1 <- t1
, CoercionTy h2 <- t2
= let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2
in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body
I'm next to positive that this code is wrong. (Maybe I wrote it -- so be it.)
Here is a concrete case. Suppose we have a coercion like
InstCo (forall (cv :: co1). ... cv ...) co3
When we process the InstCo
of the forall
, we should extend the lifting context, mapping cv
to co3
. But the second chunk of code above calls extendLiftingContext
, which extends the LiftCoEnv
portion of the lifting context, not the TCvSubst
portion, which is what the CoVarCo
case looks in. (It should look there, in case cv
is in scope from before the forall and is mapped in the ambient substitution being applied during optimization. It just shouldn't look in the TCvSubst
first.)
So the case above will fail to substitute cv
and leave us a linting problem. forall
s over coercions are rare these days, so I'm not surprised we've never seen this live. But we will someday.