Likely bug in coercion optimization

GHC.Core.Coercion.Opt contains

opt_co4 env sym rep r (CoVarCo cv)
  | ...
  | otherwise
  = assert (isCoVar cv1 )
    wrapRole rep r $ wrapSym sym $
    CoVarCo cv1

  where
    cv1 = case lookupInScope (lcInScopeSet env) cv of
             Just cv1 -> cv1
             Nothing  -> warnPprTrace True
                          (text "opt_co: not in scope:" <+> ppr cv $$ ppr env)
                          cv
          -- cv1 might have a substituted kind!

Note that instead of returning cv, this code returns cv1, the covar yanked from the in-scope set. According to the comment, this is done because the covar might have a substituted kind. Presumably, the author of that comment thinks the version of cv in the in-scope set will indeed have a substituted kind. If the covar is locally bound in a ForAllCo, this assumption is valid: we see that substForAllCoCoVarBndrUsing indeed adds new_var to the in-scope set. But what if the covar is free? I'm unaware of any invariant on TCvSubsts that says their in-scope sets contain variables with substituted kinds. (Maybe we should add that? Probably not: it would force the in-scope set considerably more often than it gets forced today, according to the comment on subst_ty.) Contrast with GHC.Core.Subst.Subst, which explicitly states that its InScopeSet is post-substitution.

Bottom line: we should just subst in the kind of cv and not bother with the InScopeSet, whose relationship to the subst is undetermined. (Or, we decide on an invariant for in-scope sets, make sure to uphold that invariant, and then take advantage of it here.)

I do not have an example that demonstrates the problem (which would likely show up only under -dcore-lint), but I'm pretty sure this is a real bug.