Free variable finders are confused about coercion holes
Definition. A deep traversal to collect free variables means that the traversal collects also the free variables in the kinds of free variables. These are also sometimes called the deep free variables.
When collecting free variables deeply of a type, GHC does a strange thing when recurring into the kinds of the variables: it zaps the set of in-scope variables, as documented in Note [Closing over free variable kinds] in GHC.Core.TyCo.Rep (and summarized in this para). For example, if we are collecting the free variables of forall a b. a -> b -> Proxy c
, we do not want to return a
and b
as free variables. We thus remember these as locally in scope, so that we skip occurrences. However, we do not want to retain a
and b
as in scope when traversing the kind of c
. Why not? Let's imagine c :: Either a b
, so that we have forall a b. a -> b -> Proxy (c :: Either a b)
. Now, are a
and b
free? Yes! That's because c
is not locally bound -- it must have come into scope previously. Accordingly, the a
and b
in its kind are not the a
and b
bound by that forall
we're all looking at -- they also must be bound further up. The simple solution is to drop the in-scope set when traversing a free variable kind. This is implemented today.
The problem is for coercion holes. (The problem presumably also happens for metavariables, but it came up in the context of coercion holes.) Specifically, look at this function:
-- | Returns free variables of Implication as a composable FV computation.
-- See Note [Deterministic FV] in "GHC.Utils.FV".
tyCoFVsOfImplic :: Implication -> FV
-- Only called on *zonked* things
tyCoFVsOfImplic (Implic { ic_skols = skols
, ic_given = givens
, ic_wanted = wanted })
| isEmptyWC wanted
= emptyFV
| otherwise
= tyCoFVsVarBndrs skols $
tyCoFVsVarBndrs givens $
tyCoFVsOfWC wanted
In the main body of this function, we bind the skolems and the givens and then traverse (deeply) the wanteds. The fact that we bind the skolems and the givens means that skolems and givens will not be considered free (good). But now consider this:
forall a. [W] hole_abc :: a ~ Bool
[W] hole_def :: ... |> hole_abc ...
When traversing the type of hole_abc
, we see that the a
is a skolem and refuse to add it to the fv set. Good. But when traversing the type of hole_def
, we see an occurrence of hole_abc
and then look in its type without an in-scope set. So we report a
as free! Disaster!
The root problem here is that coercion holes (resp. metavariables) aren't really bound. They are local to a certain TcLevel, which could in theory be used to know whether to consider them "bound-like" or "free-like" (i.e. the level could be used to set whether to zap the in-scope set when traversing an occurrence's kind), but that would add considerable complication to free-variable finding.
There is not, as far as I know, a live bug around this issue. That's because the implementation doesn't meet the specification, as we can see in this code:
tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
= tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
tyCoFVsOfCoVar v fv_cand in_scope acc
= (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
Note that the in_scope
set is not zapped when recurring in varType v
. So, despite the logic at the top of this post, we don't actually apply it in tyCoFVsOfCoVar
. (We do apply it in lots of other places.) Interestingly, the lack of zapping affects ordinary covars, not just coercion holes, and so is quite possibly a bug-in-waiting. (We just don't have enough locally bound covars to notice.)
My Tweag intern @yiyunliu is revamping free-variable finders. In his new version, he fixed the bug, but then that caused the "Disaster!" described above. (If it's helpful, I imagine he can provide more concrete details.)
I think the right answer here is to add the zapping logic to the recurrence into covar kinds, but then also to add logic to tyCoFVsOfImplic
to consider the coercion holes bound when traversing the types of the wanteds in a WC. Then, the free-var finder won't traverse the holes' kinds at all, avoiding the problem described here.
This whole area still makes me nervous though: given that a coercion hole (resp. metavariable) stands for an as-yet-unknown coercion (resp. type), taking the free variables of any type that has holes (metavars) seems dodgy, even though it's quite useful.