[GHC] #15378: Use TcLevels to decide about floating out of implications

[GHC]

#15378: Use TcLevels to decide about floating out of implications
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15378>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler