[GHC] #10185: Coercible solver incomplete with non-variable transitivity

[GHC]

#10185: Coercible solver incomplete with non-variable transitivity
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  low               |               Milestone:  ⊥
       Component:  Compiler          |                 Version:  7.11
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by Richard Eisenberg <eir@…>):

 In [changeset:"c1edbdfd9148ad9f74bfe41e76c524f3e775aaaa/ghc"]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="c1edbdfd9148ad9f74bfe41e76c524f3e775aaaa"
 Do proper depth checking in the flattener to avoid looping.

 This implements (roughly) the plan put forward in comment:14:ticket:7788,
 fixing #7788, #8550, #9554, #10139, and addressing concerns raised in
 #10079.
 There are some regressions w.r.t. GHC 7.8, but only with pathological type
 families (like F a = F a). This also (hopefully -- don't have a test case)
 fixes #10158. Unsolved problems include #10184 and #10185, which are both
 known deficiencies of the approach used here.

 As part of this change, the plumbing around detecting infinite loops has
 changed. Instead of -fcontext-stack and -ftype-function-depth, we now have
 one combined -freduction-depth parameter. Setting it to 0 disbales the
 check, which is now the recommended way to get (terminating) code to
 typecheck in releases. (The number of reduction steps may well change
 between
 minor GHC releases!)

 This commit also introduces a new IntWithInf type in BasicTypes
 that represents an integer+infinity. This type is used in a few
 places throughout the code.

 Tests in
   indexed-types/should_fail/T7788
   indexed-types/should_fail/T8550
   indexed-types/should_fail/T9554
   indexed-types/should_compile/T10079
   indexed-types/should_compile/T10139
   typecheck/should_compile/T10184  (expected broken)
   typecheck/should_compile/T10185  (expected broken)

 This commit also changes performance testsuite numbers, for the better.
 }}}

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