#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 ):
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
