Improve constraint floating
TcSimplify.flaotEqualities
is more complicated than it
needs to be. Esp see Note [What prevents a constraint from floating]
.
-
We only even try to float constraints if there are no given equalities. If there are no given equalities, then such equalities cannot capture an otherwise-floatable equality! So (2) and (3) in the Note are vacuously true.
-
But "no given equalities" should include quantified constraints! This is a bug in
getNoGivenEqs
-
Is it possible that a candidate floatable constraint mentions a Wanted coercion variable? That is, point (4) of the Note? Yes, see #14584 (closed), and remember that we don't float insoluble equalities; and they may turn into deferred type errors, and so must be in scope.
So if an equality E mentions a coercion hole for non-floated equality E2, then E can't float either. And we need to do this transitively. How annoying.
An alternative: float all nominal equalities uless they are captured by a skolem.
-
When checking for disjointness with the skolems, we can just check that the two types are OK:
- Skolem tyvar: not one of the skolems (no need to look in its kind)
- Unification var: its kind is OK
- Coercion: free covars are OK, and (maybe) types are ok