Opened 18 months ago

Last modified 13 months ago

#15378 new task

Use TcLevels to decide about floating out of implications

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.4.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (2)

comment:1 Changed 18 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for in GHC 8.6.

comment:2 Changed 13 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.