Use TcLevels to decide about floating out of implications
If we have an implication constraint forall[3] sk[3]. [W] alpha[2] ~ Maybe b[2], GHC floats the constraint out of the implication. This is necessary to solve this particular wanted, because the implication is at level 3, while the unification variable alpha is at level 2; the variable is thus untouchable in the implication.
Right now, computing which constraints can float out is done by looking at the free variables of the constraint and comparing against the set of skolem variables bound in the implication, like sk[3], above (among a few other places). However, there is a much easier way: just use the levels. We can look at the Wanted and determine that it can float out because the maximum level in the wanted is a 2, and the implication is level 3.
Thus, this ticket is to track that refactoring: use levels, not free variables, in determining what to float out of an implication.
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.4.3 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |