GHC: Ticket #595: Overhaul GHC's overlapping/non-exhaustive pattern checking
http://ghc.haskell.org/trac/ghc/ticket/595
<p>
GHC has a module in the desugarer (Check) which checks whether patterns are overlapping and/or exhaustive, to support the flags -fwarn-overlapping-patterns and -fwarn-non-exhaustive-patterns. The code is old and crufty, and has several outstanding bugs. A rewrite is needed.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/595
Trac 1.0.9simonmarThu, 08 Dec 2005 14:46:19 GMTcomponent, description changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:1
http://ghc.haskell.org/trac/ghc/ticket/595#comment:1
<ul>
<li><strong>component</strong>
changed from <em>None</em> to <em>Compiler</em>
</li>
<li><strong>description</strong>
modified (<a href="/trac/ghc/ticket/595?action=diff&version=1">diff</a>)
</li>
</ul>
TicketsimonmarThu, 15 Dec 2005 10:59:02 GMTdifficulty, os, architecture set
http://ghc.haskell.org/trac/ghc/ticket/595#comment:2
http://ghc.haskell.org/trac/ghc/ticket/595#comment:2
<ul>
<li><strong>difficulty</strong>
set to <em>Difficult (1 week)</em>
</li>
<li><strong>os</strong>
set to <em>Unknown</em>
</li>
<li><strong>architecture</strong>
set to <em>Unknown</em>
</li>
</ul>
TicketiglooFri, 20 Oct 2006 16:05:43 GMTkeywords, testcase, milestone set
http://ghc.haskell.org/trac/ghc/ticket/595#comment:3
http://ghc.haskell.org/trac/ghc/ticket/595#comment:3
<ul>
<li><strong>keywords</strong>
<em>warnings</em> added
</li>
<li><strong>testcase</strong>
set to <em>N/A</em>
</li>
<li><strong>milestone</strong>
set to <em>_|_</em>
</li>
</ul>
TicketsimonmarMon, 07 May 2007 09:19:01 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:4
http://ghc.haskell.org/trac/ghc/ticket/595#comment:4
<p>
Related tickets: <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/29" title="bug: Check for exhaustive patterns is broken (closed: invalid)">#29</a>, <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/322" title="bug: fromInteger-related pattern match overlap warnings (closed: duplicate)">#322</a>, <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/851" title="bug: Incomplete-pattern checking for n+k patterns is not implemented (closed: wontfix)">#851</a>, <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1307" title="bug: Warning refers to code not in the source (closed: duplicate)">#1307</a>
</p>
TicketsimonpjThu, 03 Jan 2008 15:19:39 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:5
http://ghc.haskell.org/trac/ghc/ticket/595#comment:5
<p>
And <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2006" title="bug: unreachable GADT pattern clauses show up as warnings with -Wall (closed: fixed)">#2006</a>
</p>
TicketsimonpjWed, 09 Apr 2008 15:51:12 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:6
http://ghc.haskell.org/trac/ghc/ticket/595#comment:6
<p>
And <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2204" title="feature request: Improve 'patterns not matched' warnings (closed: duplicate)">#2204</a>
</p>
TicketsimonmarMon, 14 Jul 2008 14:33:09 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:7
http://ghc.haskell.org/trac/ghc/ticket/595#comment:7
<p>
And <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/366" title="feature request: incomplete patterns and GADT (closed: fixed)">#366</a>.
</p>
<p>
Someone could fix this and bag 8 tickets in one go :-)
</p>
TicketsimonmarTue, 30 Sep 2008 15:37:14 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:8
http://ghc.haskell.org/trac/ghc/ticket/595#comment:8
<ul>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:51:01 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:9
http://ghc.haskell.org/trac/ghc/ticket/595#comment:9
<ul>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonpjMon, 09 Mar 2009 14:44:21 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:10
http://ghc.haskell.org/trac/ghc/ticket/595#comment:10
<p>
Also look at <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3078" title="bug: Erroneous warnings for -XPatternGuards (closed: duplicate)">#3078</a>: pattern guards.
</p>
TicketsimonmarMon, 16 Nov 2009 13:14:44 GMTdifficulty changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:11
http://ghc.haskell.org/trac/ghc/ticket/595#comment:11
<ul>
<li><strong>difficulty</strong>
changed from <em>Difficult (1 week)</em> to <em>Difficult (2-5 days)</em>
</li>
</ul>
TicketiglooSat, 02 Jan 2010 21:27:27 GMTfailure set
http://ghc.haskell.org/trac/ghc/ticket/595#comment:12
http://ghc.haskell.org/trac/ghc/ticket/595#comment:12
<ul>
<li><strong>failure</strong>
set to <em>Incorrect warning at compile-time</em>
</li>
</ul>
TicketmarcotmarcotThu, 28 Jan 2010 23:17:17 GMTowner set
http://ghc.haskell.org/trac/ghc/ticket/595#comment:13
http://ghc.haskell.org/trac/ghc/ticket/595#comment:13
<ul>
<li><strong>owner</strong>
set to <em>marcotmarcot</em>
</li>
</ul>
<p>
I'm studying the source code related to the bug, and I have read the <a class="ext-link" href="http://pauillac.inria.fr/~maranget/papers/warn/index.html"><span class="icon"></span>pointed paper</a>. I'm <a class="ext-link" href="http://www2.dcc.ufmg.br/laboratorios/llp/wiki/doku.php?id=pattern_matching_in_ghc"><span class="icon"></span>describing my progress in this page</a>.
</p>
TicketsimonpjThu, 28 Jan 2010 23:31:46 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:14
http://ghc.haskell.org/trac/ghc/ticket/595#comment:14
<p>
Excellent! Please also consult <a class="ext-link" href="http://www.cs.cmu.edu/~neelk/pattern-popl09.pdf"><span class="icon"></span>http://www.cs.cmu.edu/~neelk/pattern-popl09.pdf</a>
</p>
<p>
Also do not forget about view patterns
</p>
<p>
Simon
</p>
TicketmarcotmarcotFri, 19 Feb 2010 18:19:15 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:15
http://ghc.haskell.org/trac/ghc/ticket/595#comment:15
<p>
Hi.
</p>
<p>
I won't work with this task, because I've not found the relevance. <a class="ext-link" href="http://hackage.haskell.org/trac/ghc/ticket/322"><span class="icon"></span>Issue #322</a> doens't seem to be fixable, and <a class="ext-link" href="http://hackage.haskell.org/trac/ghc/ticket/2204"><span class="icon"></span>issue #2204</a> and <a class="ext-link" href="http://hackage.haskell.org/trac/ghc/ticket/1307"><span class="icon"></span>#1307</a> are only about improving the error message.
</p>
<p>
Greetings.
</p>
TicketmarcotmarcotFri, 19 Feb 2010 18:19:42 GMTowner deleted
http://ghc.haskell.org/trac/ghc/ticket/595#comment:16
http://ghc.haskell.org/trac/ghc/ticket/595#comment:16
<ul>
<li><strong>owner</strong>
<em>marcotmarcot</em> deleted
</li>
</ul>
TicketmarcotmarcotFri, 19 Feb 2010 19:40:40 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/595#comment:17
http://ghc.haskell.org/trac/ghc/ticket/595#comment:17
<ul>
<li><strong>cc</strong>
<em>marcot@…</em> added
</li>
</ul>
TicketryaniFri, 27 Aug 2010 23:06:13 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:18
http://ghc.haskell.org/trac/ghc/ticket/595#comment:18
<ul>
<li><strong>cc</strong>
<em>ryani.spam@…</em> added
</li>
</ul>
Ticketbross279Mon, 26 Mar 2012 07:38:02 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:19
http://ghc.haskell.org/trac/ghc/ticket/595#comment:19
<ul>
<li><strong>cc</strong>
<em>benjross@…</em> added
</li>
</ul>
<p>
Is anyone working on this? This project interests me for GSoC, and I was wondering who I could talk to to find more information on this project.
</p>
TicketsimonpjTue, 27 Mar 2012 08:50:03 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:20
http://ghc.haskell.org/trac/ghc/ticket/595#comment:20
<p>
No, no one is working on it, as far as I know, and I would love someone to pay attention to it. There are a bunch of related tickets: at least <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/595" title="task: Overhaul GHC's overlapping/non-exhaustive pattern checking (closed: fixed)">#595</a>, <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5728" title="bug: Warnings from -fwarn-incomplete-record-updates even with all ... (closed: duplicate)">#5728</a>, <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3927" title="bug: Incomplete/overlapped pattern warnings + GADTs = inadequate (closed: duplicate)">#3927</a>, <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5724" title="bug: Confusing warning message for incomplete patterns (closed: duplicate)">#5724</a>, <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5762" title="bug: GHC gives incorrect warnings with simple applications of the view ... (closed: duplicate)">#5762</a>, <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4139" title="bug: Spurious non-exhaustive pattern match warnings are given using GADTs (closed: duplicate)">#4139</a>. It has the great merit of being a nicely-separable task, one that doesn't interact with the rest of GHC.
</p>
<p>
There is a good literature to guide you:
</p>
<ul><li>Several papers by Luc Maranget, including a JFP paper <a class="ext-link" href="http://moscova.inria.fr/~maranget/papers/warn/index.html"><span class="icon"></span>Warnings for patttern matching</a>
</li><li>Neel Krishnaswami <a class="ext-link" href="http://www.cs.cmu.edu/~neelk/pattern-popl09.pdf"><span class="icon"></span>Focusing on pattern matching</a>
</li></ul><p>
However these papers focus entirely on a "block" of pattern matching, for example, a function defined by pattern matching. Many of the tickets go further:
</p>
<ul><li>Consider
<pre class="wiki">f xs@(y:ys) = .....case xs of { (y:ys) -> ... }
</pre>The inner pattern match should not complain about a missing nil case. You may think this is a silly program, but it's less silly when record updates are concerned.
</li></ul><ul><li>Matches that involve GADTs. Here things are a bit more complicated, and involve figuring out what branches are inaccessible because of type constraints. It's not that hard, but generating good warnings goes beyond what the literature covers.
</li></ul><p>
I don't want to supervise this, but would would be happy to offer advice and guidance about GHC aspects, if someone else would lead.
</p>
TicketcarterSun, 01 Sep 2013 21:04:40 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:21
http://ghc.haskell.org/trac/ghc/ticket/595#comment:21
<ul>
<li><strong>cc</strong>
<em>carter.schonwald@…</em> added
</li>
</ul>
TicketrefoldMon, 02 Sep 2013 17:18:11 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:22
http://ghc.haskell.org/trac/ghc/ticket/595#comment:22
<ul>
<li><strong>cc</strong>
<em>the.dead.shall.rise@…</em> added
</li>
</ul>
TicketjkarniTue, 11 Feb 2014 04:56:53 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:23
http://ghc.haskell.org/trac/ghc/ticket/595#comment:23
<ul>
<li><strong>cc</strong>
<em>jkarni@…</em> added
</li>
</ul>
TicketmbassettSun, 30 Mar 2014 12:55:39 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:24
http://ghc.haskell.org/trac/ghc/ticket/595#comment:24
<ul>
<li><strong>cc</strong>
<em>michael.b.bassett@…</em> added
</li>
</ul>
TicketcheecheeoThu, 01 Oct 2015 21:50:51 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:25
http://ghc.haskell.org/trac/ghc/ticket/595#comment:25
<ul>
<li><strong>cc</strong>
<em>cheecheeo@…</em> added
</li>
</ul>
TicketlelfMon, 26 Oct 2015 10:32:30 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:26
http://ghc.haskell.org/trac/ghc/ticket/595#comment:26
<ul>
<li><strong>cc</strong>
<em>lelf</em> added
</li>
</ul>
TicketgkarachaTue, 01 Dec 2015 23:41:48 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:27
http://ghc.haskell.org/trac/ghc/ticket/595#comment:27
<ul>
<li><strong>cc</strong>
<em>george.karachalias@…</em> added
</li>
</ul>
TicketGeorge Karachalias <george.karachalias@…>Thu, 03 Dec 2015 11:58:00 GMT
http://ghc.haskell.org/trac/ghc/ticket/595#comment:28
http://ghc.haskell.org/trac/ghc/ticket/595#comment:28
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/8a506104d5b5b71d5640afc69c992e0af40f2213/ghc" title="Major Overhaul of Pattern Match Checking (Fixes #595)
This patch ...">8a506104/ghc</a>:
</p>
<pre class="message">Major Overhaul of Pattern Match Checking (Fixes #595)
This patch adresses several problems concerned with exhaustiveness and
redundancy checking of pattern matching. The list of improvements includes:
* Making the check type-aware (handles GADTs, Type Families, DataKinds, etc.).
This fixes #4139, #3927, #8970 and other related tickets.
* Making the check laziness-aware. Cases that are overlapped but affect
evaluation are issued now with "Patterns have inaccessible right hand side".
Additionally, "Patterns are overlapped" is now replaced by "Patterns are
redundant".
* Improved messages for literals. This addresses tickets #5724, #2204, etc.
* Improved reasoning concerning cases where simple and overloaded
patterns are matched (See #322).
* Substantially improved reasoning for pattern guards. Addresses #3078.
* OverloadedLists extension does not break exhaustiveness checking anymore
(addresses #9951). Note that in general this cannot be handled but if we know
that an argument has type '[a]', we treat it as a list since, the instance of
'IsList' gives the identity for both 'fromList' and 'toList'. If the type is
not clear or is not the list type, then the check cannot do much still. I am
a bit concerned about OverlappingInstances though, since one may override the
'[a]' instance with e.g. an '[Int]' instance that is not the identity.
* Improved reasoning for nested pattern matching (partial solution). Now we
propagate type and (some) term constraints deeper when checking, so we can
detect more inconsistencies. For example, this is needed for #4139.
I am still not satisfied with several things but I would like to address at
least the following before the next release:
Term constraints are too many and not printed for non-exhaustive matches
(with the exception of literals). This sometimes results in two identical (in
appearance) uncovered warnings. Unless we actually show their difference, I
would like to have a single warning.</pre>
TicketadamgundryWed, 30 Dec 2015 12:46:42 GMTstatus, resolution, milestone changed
http://ghc.haskell.org/trac/ghc/ticket/595#comment:29
http://ghc.haskell.org/trac/ghc/ticket/595#comment:29
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
changed from <em>None</em> to <em>fixed</em>
</li>
<li><strong>milestone</strong>
changed from <em>⊥</em> to <em>8.0.1</em>
</li>
</ul>
<p>
Great work @gkaracha!
</p>
Ticket