[GHC] #9318: Type error reported in wrong place with repeated type family expressions

[GHC]

#9318: Type error reported in wrong place with repeated type family expressions
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:  simonpj
                  Type:  bug         |            Status:  new
              Priority:  high        |         Milestone:  7.10.1
             Component:  Compiler    |           Version:  7.8.3
  (Type checker)                     |          Keywords:
            Resolution:              |  Operating System:  Unknown/Multiple
Differential Revisions:              |   Type of failure:  None/Unknown
          Architecture:              |         Test Case:
  Unknown/Multiple                   |          Blocking:
            Difficulty:  Unknown     |
            Blocked By:              |
       Related Tickets:              |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * cc: dimitris@… (added)
 * owner:   => simonpj
 * priority:  normal => high
 * milestone:   => 7.10.1


Comment:

 Dimitrios, I'd like to discuss this with you when you get back.

 The behaviour is terrible, and it's a classic case of rewriting a wanted
 with a wanted.  We have
 {{{
 [W] w1 :: F Int ~ Bool   -- From foo
 [W] w2 :: F Int ~ Char   -- From bar
 }}}
 We try to solve `w2` first:
  * we rewrite the `F Int` to `Bool`,
  * add `w2` to the `inert_solved_funeqs`
  * make `w3` :: Bool ~ Char`  (insoluble, correctly)
  * bind `w2` to evidence involving `w3` and the axiom

 But now when we try to solve `w1` we find `w2` in the
 `inert_solved_funeqs` before looking up in the axioms, and thus rewrite to
 `Char ~ Bool`.  Disaster.

 The problem is putting `w2` (which is really insoluble) in the
 `inert_solved_funeqs`.

 Instead I suspect we should put only ''givens'' in the
 `inert_solved_funeqs`, namely the evidence from the use of the axiom.  So
 solving the second goal would go more like this
  * we rewrite the `F Int` to `Bool`, with coercion `co`
  * add `[G] co : F Int ~ Bool` to `inert_solved_funeqs`
  * create `[W] w3 :: Bool ~ Char`
  * bind `w2 = co ; w3`

 Now `inert_solved_funeqs` contains only givens derived directly from
 axioms, which we can safely use to solve anything.

 Simon

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