Opened 2 years ago

Closed 2 years ago

#11160 closed bug (fixed)

New exhaustiveness checker breaks ghcirun004

Reported by: bgamari Owned by:
Priority: high Milestone: 8.2.1
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:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

The new exhaustiveness checker (8a506104d5b5b71d5640afc69c992e0af40f2213, Phab:D1535) has broken tests/ghci/should_run/ghcirun004, which now hangs in desugaring. If one removes all but a few hundred of foo's equations in the test things return to sanity. It appears that the compile time is scaling non-linearly with the number of equations,

no. equations compile wall time
150 0.4 s
250 0.89 s
300 1.22 s
350 1.85 s
400 2.65 s
500 4.86 s
550 6.60 s
600 8.65 s
650 10.27 s
700 12.84 s
1000 38.51 s

Change History (12)

comment:1 Changed 2 years ago by bgamari

Cc: gkarachalias added
Description: modified (diff)
Milestone: 8.0.1

comment:2 Changed 2 years ago by bgamari

The cost here comes from pruneVSABound, in particular the Singleton case in go.

comment:3 Changed 2 years ago by bgamari

More specifically it seems to be TmOracle.tmOracle which is the culprit. Perhaps this is one of these terrible worst-cases which the paper refers to?

comment:4 Changed 2 years ago by gkaracha

Cc: gkaracha added; gkarachalias removed

comment:5 Changed 2 years ago by bgamari

Owner: set to gkaracha

George thinks he has this one figured out and will work out a fix shortly.

comment:6 Changed 2 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
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!).

comment:7 Changed 2 years ago by simonpj

Very fast response thank you.

Your commit message is very informative. Did you include the same information in a Note in the code, so that we don't lose the information here?

comment:8 Changed 2 years ago by bgamari

Description: modified (diff)
Resolution: fixed
Status: newclosed

comment:9 in reply to:  7 Changed 2 years ago by gkaracha

Your commit message is very informative. Did you include the same information in a Note in the code, so that we don't lose the information here?

Done. I have added two separate notes:

comment:10 Changed 2 years ago by simonpj

Keywords: PatternMatchWarnings added
Milestone: 8.0.18.2.1

I'm re-opening with a milestone of 8.2, because I really think we can do better, and I don't want to lose track of the example. But it's not pressing for 8.0.

comment:11 Changed 2 years ago by simonpj

Owner: gkaracha deleted
Resolution: fixed
Status: closednew

comment:12 Changed 2 years ago by gkaracha

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