decideMonoTyVars doesn't handle coercion variables in "candidates"
In decideMonoTyVars
we find:
mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
tyCoVarsOfTypes candidates
...
co_vars = coVarsOfTypes (psig_tys ++ taus)
mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
...
mono_tvs2 = closeWrtFunDeps non_ip_candidates mono_tvs1
Note that closeWrtFunDeps
expects a set of type variables closed over kinds. However, mono_tvs1
doesn't seem to be closed over kinds, in general:
-
tyCoVarsOfTypes
is deep, sotyCoVarsOfTypes candidates
is closed over kinds. - We filter out some variables using
isQuantifiableTv
. How do we know this set is still closed over kinds? In particular, we might have kept a coercion variable but not the type variables found in its kind.
I ran into the following example while working on a patch:
Candidates:
{co} :: gamma[conc] ~# F
alpha[tau:1] ~# (beta[tau:1] |> TYPE {co})
At TcLevel
0, mono_tvs0 = {co}
, closeOverKinds mono_tvs0 = {co, gamma}
.
@rae, what am I missing? Is the above collection of candidates somehow ill-formed, i.e. doesn't uphold some invariant required to pass it to decideMonoTyVars
?