GitLab

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. foralls over coercions are rare these days, so I'm not surprised we've never seen this live. But we will someday.