Opened 4 years ago

Closed 4 years ago

#11161 closed bug (fixed)

New exhaustiveness checker breaks concurrent/prog001

Reported by: bgamari Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.2
Keywords: PatternMatchWarnings Cc: gkaracha
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case: concurrent/prog001
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

The new exhaustiveness checker appears to allocate until the machine runs out of memory while compiling the concurrent/prog001 testcase. In particular it stalls while desugaring the Thread module. The fact that this module contains non-trivial pattern matching, coupled with the compiler gets stuck in Desugar, and the fact that I've noted other performance issues with the new exhaustiveness checker (see #11160) leads me to believe that this patch is to blame.

Change History (6)

comment:1 Changed 4 years ago by bgamari

Cc: gkaracha added
Description: modified (diff)
Owner: set to gkaracha

comment:2 Changed 4 years ago by George Karachalias <george.karachalias@…>

In ae4398d/ghc:

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

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,

comment:3 Changed 4 years ago by bgamari

Resolution: fixed
Status: newclosed

This is fixed.

comment:4 Changed 4 years ago by simonpj

Keywords: PatternMatchWarnings added
Owner: gkaracha deleted
Resolution: fixed
Status: closednew

Re-opening to improve for 8.2

comment:5 Changed 4 years ago by thomie

Milestone: 8.0.1

comment:6 Changed 4 years ago by gkaracha

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.