[GHC] #15009: Float equalities past local equalities

[GHC]

#15009: Float equalities past local equalities
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  feature request   |               Status:  closed
        Priority:  normal            |            Milestone:  8.4.3
       Component:  Compiler          |              Version:  8.2.2
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:  gadt/T15009
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 What, precisely, is the rule you propose?  I don't know precisely what
 "float equalities past equalities if the involved levels are OK" means.

 I think you mean something like "you can float a wanted equality W
 past a given equality G iff that G not to be used in any solution of
 W.

 But it's hard to come up with an implementation of that rule, other
 than "don't float past equalities".  Whatever we choose must be
 simple and predictable.

 I worry about things like this
 {{{
 Implic { TcLevel = 3
        , Skolems = []
        , Given = (y ~ Bool, F y Int ~ Char)
        , Wanted = z[tau:2] ~ F Bool t[tau:1]
        }
 }}}
 Can I float that wanted?  Well, no.  Maybe, later, we'll discover that `t
 := Int`.
 Then our `F Bool Int` can be rewritten to `F y Int` (with the local
 equality), and
 thence to Char.  But if we floated it out we'd get stuck.

 If you have a better rule, that'd be great.  I just don't see it yet.

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