GHC: Ticket #4139: Spurious non-exhaustive pattern match warnings are given using GADTs
http://ghc.haskell.org/trac/ghc/ticket/4139
<p>
When using slightly complicated GADTs, GHC gives me erroneous non-exhaustive pattern match warnings. I have attached an example. I have observed this behavior in the four versions of ghc that I tried (6.10.4, and 6.12.{1,2,3}).
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/4139
Trac 1.2.2.dev0blarsenWed, 16 Jun 2010 16:24:38 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/4139
http://ghc.haskell.org/trac/ghc/ticket/4139
<ul>
<li><strong>attachment</strong>
set to <em>GADTNonExhaustive.hs</em>
</li>
</ul>
<p>
A simple evaluator that demonstrates spurious non-exhaustive pattern match warnings
</p>
TicketiglooThu, 17 Jun 2010 23:21:51 GMTowner, milestone set
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:1
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:1
<ul>
<li><strong>owner</strong>
set to <em>simonpj</em>
</li>
<li><strong>milestone</strong>
set to <em>6.14.1</em>
</li>
</ul>
<p>
Thanks for the report.
</p>
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3927" title="#3927: bug: Incomplete/overlapped pattern warnings + GADTs = inadequate (closed: duplicate)">#3927</a>.
</p>
TicketsimonpjTue, 21 Sep 2010 21:33:18 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:2
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:2
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>invalid</em>
</li>
</ul>
<p>
Now I look at your example, I see that your claim isn't true! Consider
</p>
<pre class="wiki">evalFst (Const (undefined :: Const (Int,Int))
</pre><p>
That will hit the allegedly impossible alternative.
</p>
<p>
So in this case GHC is quite right. (The pattern match warnings are not all correct, but this one is, I think.)
</p>
<p>
Simon
</p>
TicketblarsenWed, 22 Sep 2010 03:35:56 GMT
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:3
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:3
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4139#comment:2" title="Comment 2">simonpj</a>:
</p>
<blockquote class="citation">
<p>
Now I look at your example, I see that your claim isn't true! Consider
</p>
<pre class="wiki">evalFst (Const (undefined :: Const (Int,Int))
</pre><p>
That will hit the allegedly impossible alternative.
</p>
<p>
So in this case GHC is quite right. (The pattern match warnings are not all correct, but this one is, I think.)
</p>
<p>
Simon
</p>
</blockquote>
<p>
Indeed! I had forgotten about undefined / bottom values.
</p>
<p>
Brad
</p>
TicketgoldfireMon, 13 Feb 2012 18:23:54 GMTstatus, failure, version changed; cc set; owner, resolution deleted
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:4
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:4
<ul>
<li><strong>status</strong>
changed from <em>closed</em> to <em>new</em>
</li>
<li><strong>cc</strong>
<em>eir@…</em> added
</li>
<li><strong>failure</strong>
changed from <em>None/Unknown</em> to <em>Incorrect warning at compile-time</em>
</li>
<li><strong>version</strong>
changed from <em>6.12.3</em> to <em>7.4.1</em>
</li>
<li><strong>owner</strong>
<em>simonpj</em> deleted
</li>
<li><strong>resolution</strong>
<em>invalid</em> deleted
</li>
</ul>
<p>
I have a case with the same bug description as above, but when I include the pattern suggested by the warning statement, I get a compiler error indicating unreachable code. I have attached my code.
</p>
TicketgoldfireMon, 13 Feb 2012 18:24:38 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/4139
http://ghc.haskell.org/trac/ghc/ticket/4139
<ul>
<li><strong>attachment</strong>
set to <em>GADTbug.hs</em>
</li>
</ul>
<p>
produces warning about non-exhaustive pattern match in GADT
</p>
TicketsimonpjWed, 15 Feb 2012 17:13:18 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:5
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:5
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
Good example. It has the same cause as <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3927" title="#3927: bug: Incomplete/overlapped pattern warnings + GADTs = inadequate (closed: duplicate)">#3927</a>. Sorry no imminent cure. Needs someone to pay proper attention to it.
</p>
TicketgoldfireWed, 16 May 2012 20:17:18 GMTrelated set
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:6
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:6
<ul>
<li><strong>related</strong>
set to <em>#3927</em>
</li>
</ul>
TicketliyangFri, 22 Mar 2013 10:18:40 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:7
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:7
<ul>
<li><strong>cc</strong>
<em>hackage.haskell.org@…</em> added
</li>
</ul>
TicketezyangMon, 30 Jun 2014 13:37:54 GMTmilestone deleted
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:8
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:8
<ul>
<li><strong>milestone</strong>
<em>7.0.1</em> deleted
</li>
</ul>
TicketthomieWed, 05 Aug 2015 16:59:02 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:9
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:9
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>duplicate</em>
</li>
</ul>
<p>
Because the existence of duplicate tickets makes doing a <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/BugSweep">BugSweep</a> of the bug tracker more cumbersome, I'm closing these tickets as duplicate. Don't worry, they're still listed on <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/PatternMatchCheck">PatternMatchCheck</a>, and will hopefully all be addressed by the <a class="ext-link" href="http://git.haskell.org/ghc.git/shortlog/refs/heads/wip/gadtpm"><span class="icon"></span>work</a> on <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/595" title="#595: task: Overhaul GHC's overlapping/non-exhaustive pattern checking (closed: fixed)">#595</a> ("Overhaul GHC's overlapping/non-exhaustive pattern checking").
</p>
<ul><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/322" title="#322: bug: fromInteger-related pattern match overlap warnings (closed: duplicate)">#322</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1307" title="#1307: bug: Warning refers to code not in the source (closed: duplicate)">#1307</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3927" title="#3927: bug: Incomplete/overlapped pattern warnings + GADTs = inadequate (closed: duplicate)">#3927</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4139" title="#4139: bug: Spurious non-exhaustive pattern match warnings are given using GADTs (closed: duplicate)">#4139</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5728" title="#5728: bug: Warnings from -fwarn-incomplete-record-updates even with all ... (closed: duplicate)">#5728</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5762" title="#5762: bug: GHC gives incorrect warnings with simple applications of the view ... (closed: duplicate)">#5762</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/6124" title="#6124: bug: Spurious non-exhaustive warning with GADT and newtypes (closed: duplicate)">#6124</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/7669" title="#7669: bug: Empty case causes warning (closed: duplicate)">#7669</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8494" title="#8494: feature request: Warn if a pattern guard obviates all others (closed: duplicate)">#8494</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8853" title="#8853: bug: Surprising mention of unboxed integers in pattern exhaustiveness warning (closed: duplicate)">#8853</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8970" title="#8970: bug: Non-exhaustive pattern match warning with DataKinds and TypeFamilies (closed: duplicate)">#8970</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9113" title="#9113: bug: Template Haskell should warn about non-exhaustive pattern matches (closed: duplicate)">#9113</a>
</li><li><a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9951" title="#9951: bug: OverloadedLists breaks exhaustiveness check (closed: duplicate)">#9951</a>
</li></ul>
TicketGeorge Karachalias <george.karachalias@…>Thu, 03 Dec 2015 11:58:00 GMT
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:10
http://ghc.haskell.org/trac/ghc/ticket/4139#comment:10
<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>
Ticket