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:
-
tyCoVarsOfTypesis deep, sotyCoVarsOfTypes candidatesis 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] ~# Falpha[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?
Edited by sheaf