[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 nfrisby):

 Replying to [comment:5 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
 > }}}

 How is it that {{{a_a2do}}} occurs both as {{{a_a2do[sk:2]}}} and also as
 {{{a_a2do[tau:2]}}} in this implication tree?

 I'm still working on a response to your suggested edit of the Note, but
 while I was rereading your comments I noticed the above. I'm surprised to
 see the same type variable (by unique at least) occurring with two
 different forms of `Details`. Seems like I'm missing some relevant
 concept. The Notes in TcType didn't seem relevant or didn't discuss it.

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