#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