[GHC] #9117: Coercible constraint solver misses one

[GHC]

#9117: Coercible constraint solver misses one
-------------------------------------+------------------------------------
        Reporter:  goldfire          |            Owner:  nomeata
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by goldfire):

 You've revealed yet another interesting characteristic of this algorithm.
 The order ''of the coercion'' matters!

 Here is my test case:

 {{{
 newtype Rec a = Rec (Rec a)
 newtype Hide a = Hide (Rec a)

 ex :: Hide Age -> Rec Int
 ex = coerce
 }}}

 (Note -- no module boundary.) This example (on GHC 7.8.2, without the
 updated solver earlier in this ticket) works fine. If I reverse the order
 of the coercion, though, it fails. This, of course, makes sense when
 thinking about the implementation, but it's weird if you don't think about
 that.

 This is all suggesting to me that the "correct" thing to do when recursion
 gets out of hand is not to immediately fail, but to try other techniques.
 I know this idea violates the maxim of "do no search", but I'm not sure
 what's so terrible about searching here.

 Getting back to your example, I posit that, with my ordering above (`Hide
 Int -> Rec Age`) the new solver will fail. This makes the new solver less
 (not?) dependent on coercion order. Is that better? Perhaps.

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