Skip to content

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:

  1. tyCoVarsOfTypes is deep, so tyCoVarsOfTypes candidates is closed over kinds.
  2. 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?

Edited by sheaf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information