[GHC] #11160: New exhaustiveness checker breaks ghcirun004
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | performance bug Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The new exhaustiveness checker 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 || -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * cc: gkarachalias (added) * milestone: => 8.0.1 Old description:
The new exhaustiveness checker 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 ||
New description: The new exhaustiveness checker (8a506104d5b5b71d5640afc69c992e0af40f2213) 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 || -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): The cost here comes from `pruneVSABound`, in particular the `Singleton` case in `go`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by gkaracha): * cc: gkarachalias (removed) * cc: gkaracha (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: gkaracha Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: => gkaracha Comment: George thinks he has this one figured out and will work out a fix shortly. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: gkaracha Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: 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/11160#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: gkaracha Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: gkaracha Type: bug | Status: closed Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed Old description:
The new exhaustiveness checker (8a506104d5b5b71d5640afc69c992e0af40f2213) 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 ||
New description: 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 || -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: gkaracha Type: bug | Status: closed Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: * About the representation of term equalities: 81cf200902628a6539572774ecc66678e133daaf * About the treatment of equality for overloaded literals: 406444b5f4173c20567abc3a3577a58a8ade10d4 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: gkaracha Type: bug | Status: closed Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 7.10.2 Resolution: fixed | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => PatternMatchWarnings * milestone: 8.0.1 => 8.2.1 Comment: 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: gkaracha => * status: closed => new * resolution: fixed => -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11160: New exhaustiveness checker breaks ghcirun004 -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: closed Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 7.10.2 Resolution: fixed | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by gkaracha): * status: new => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11160#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC