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 TCvSubst
s 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.