[GHC] #11161: New exhaustiveness checker breaks concurrent/prog001

[GHC]

#11161: New exhaustiveness checker breaks concurrent/prog001
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:  gkaracha
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Compile-time      |            Test Case:
  performance bug                    |  concurrent/prog001
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by George Karachalias <george.karachalias@…>):

 In [changeset:"ae4398d64655b43606386dddb01637bbfcf0171e/ghc" ae4398d/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="ae4398d64655b43606386dddb01637bbfcf0171e"
 Improve performance for PM check on literals (Fixes #11160 and #11161)

 Two changes:

 1. Instead of generating constraints of the form (x ~ e) (as we do in
 the paper), generate constraints of the form (e ~ e). The term oracle
 (`tmOracle` in deSugar/TmOracle.hs) is not really efficient and in the
 presence of many (x ~ e) constraints behaves quadratically. For
 literals, constraints of the form (False ~ (x ~ lit)) are pretty common,
 so if we start with { y ~ False, y ~ (x ~ lit) } we end up givng to the
 solver (a) twice as many constraints as we need and (b) half of them
 trigger the solver's weakness. This fixes #11160.

 2. Treat two overloaded literals that look different as different. This
 is not entirely correct but it is what both the previous and the current
 check did. I had the ambitious plan to do the *right thing* (equality
 between overloaded literals is undecidable in the general case) and just
 use this assumption when issuing the warnings. It seems to generate much
 more constraints than I expected (breaks #11161) so I just do it
 immediately now instead of generating everything and filtering
 afterwards.

 Even if it is not (strictly speaking) correct, we have the following:
   * Gives the "expected" warnings (the ones Ocaml or the previous
     algorithm would give) and,
   * Most importantly, it is safe. Unless a catch-all clause exists, a
     match against literals is always non-exhaustive. So, effectively
     this affects only what is shown to the user (and, evidently,
     performance!).
 }}}

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