[GHC] #15009: Float equalities past local equalities

[GHC]

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

Comment (by simonpj):

 I took a look.  Turns out that it is what I guessed:

 >  I don't say that it's perfectly implemented (eg I'm a bit worried about
 whether it's sensitive to whether the constraint looks like a ~ b or b ~
 a)

 We end up with
 {{{
 Implic {
   TcLevel = 2
   Skolems = a_a2do[sk:2] p_a2dt[sk:2]
   No-eqs = True
   Status = Unsolved
   Given =
   Wanted =
     WC {wc_impl =
           Implic {
             TcLevel = 3
             Skolems = b_a2dp[ssk:3]
             No-eqs = True
             Status = Unsolved
             Given = $d~_a2dq :: (b_a2dp[ssk:3] :: *) ~ (a_a2do[tau:2] ::
 *)
             Wanted =
               WC {wc_simple =
                     [WD] hole{co_a2dE} {1}:: (p_a2dt[sk:2] :: *)
                                              GHC.Prim.~# (Bool :: *)
 (CNonCanonical)
                     [WD] hole{co_a2dR} {1}:: (a_a2do[sk:2] :: *)
                                              GHC.Prim.~# (Bool :: *)
 (CNonCanonical)}
             a pattern with constructor:
               MkT1 :: forall b a. ((b :: *) ~ (a :: *)) => b -> T1 a
 }}}
 After expanding superclases etc, that Given `b_a2dp ~ a_a2do` turns into
 {{{
   [G] (a_a2do[tau:2] :: *) GHC.Prim.~# (b_a2dp[ssk:3] :: *)
 }}}
 with the unification variable carefully placed on the left (see
 `TcUnify.swapOverTyVars`.

 But alas `TcSMonad.getNoGivenEqs` only looks on the left in the test
 `skolem_bound_here`.  So it conservatively says "this implication may bind
 non-local equalities" and we lose.

 I see two ways to fix this

 1. Make `getNoGivenEqs` look on the right as well as the left. That, a
 Given `CTyEqCan` equality `b ~# a` would not count as a "given equality"
 if `a` is a skolem bound by this implication.

 2. Change `swapOverTyVars` so that puts the skolem (not the meta-tyvar) on
 the left for Givens.  (No change for Wanteds.)

 I think (2) is better.  I think (1) won't help at all.  Consider doing
 type inference for `f`:
 {{{
 data T1 a where
   MkT1 :: a ~ b => b -> T1 a

 f (MkT1 a) = not a
 }}}
 We decide (roughly) that `f :: T alpha[1] -> beta[1]`,
 and then simplify this implication
 {{{
 forall[2] b. (alpha[1] ~# b) => alpha[1] ~# Bool, beta[1] ~# Bool
 }}}
 (The `[1]` and `[2]` are the level numbers; `alpha[1]` is untouchable
 inside the `[2]` implication.)

 If we orient the Given as shown, with `alpha[1]` on the left, we'll
 rewrite the Wanteds thus:
 {{{
 forall[2] b. (alpha[1] ~# b) => b ~# Bool, beta[1] ~# Bool
 }}}
 And now, ''even if we say that the Given doesn't count as a "given
 equality"'', we still can't solve that `b ~# Bool`.  (We could
 float and solve `beta[1] ~# Bool`, but that's only half the problem.)

 What we want is to orient the Given the other way round `b ~# alpha[1]`.
 Then we could float out ''both'' Wanteds.  Another way to think about
 putting `b` on the left is
 that it helps to eliminate occurrences of skolems, which might prevent
 floating.

 Richard, any thoughts?

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