GHC: Ticket #3651: GADT type checking too liberal
http://ghc.haskell.org/trac/ghc/ticket/3651
<p>
I would expect the following three functions to fail:
</p>
<pre class="wiki">{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Unsafe where
data Z a where
U :: Z ()
B :: Z Bool
unsafe1 :: Z a -> Z a -> a
unsafe1 B U = ()
unsafe2 :: a ~ b => Z b -> Z a -> a
unsafe2 B U = ()
unsafe3 :: a ~ b => Z a -> Z b -> a
unsafe3 B U = True
</pre><p>
But they are all accepted. In unsafe1 it seems pattern matching on the second argument discards any information learned from pattern matching on the first, while in the other two functions it seems the equality constraints are not checked at all.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/3651
Trac 1.0.1iglooFri, 20 Nov 2009 20:35:51 GMTfailure, milestone set
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:1
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:1
<ul>
<li><strong>failure</strong>
set to <em>None/Unknown</em>
</li>
<li><strong>milestone</strong>
set to <em>6.14.1</em>
</li>
</ul>
<p>
These are all accepted in 6.12 and HEAD too, but trying to call any of them with arguments B and U fails:
</p>
<pre class="wiki">Couldn't match expected type `Bool' against inferred type `()'
</pre><p>
I'm not sure if that's the expected behaviour or not.
</p>
TicketmichaltTue, 12 Oct 2010 18:38:39 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:2
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:2
<ul>
<li><strong>cc</strong>
<em>michal.terepeta@…</em> added
</li>
</ul>
<p>
Seems like the new type checker fixes the bug:
</p>
<ul><li>for <tt>unsafe1</tt>:
</li></ul><pre class="wiki">Inaccessible code in
a pattern with constructor `U', in an equation for `unsafe1'
Couldn't match type `()' with `Bool'
In the pattern: U
In an equation for `unsafe1': unsafe1 B U = ()
</pre><ul><li>for <tt>unsafe2</tt>:
</li></ul><pre class="wiki">Inaccessible code in
a pattern with constructor `U', in an equation for `unsafe2'
Couldn't match type `()' with `Bool'
In the pattern: U
In an equation for `unsafe2': unsafe2 B U = ()
</pre><ul><li>for <tt>unsafe3</tt>:
</li></ul><pre class="wiki">Inaccessible code in
a pattern with constructor `U', in an equation for `unsafe3'
Couldn't match type `()' with `Bool'
In the pattern: U
In an equation for `unsafe3': unsafe3 B U = True
</pre><pre class="wiki">ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.1.20101008
</pre><p>
Not sure whether we should create a new test for this ticket, so I'm leaving it open.
</p>
TicketiglooWed, 13 Oct 2010 22:06:47 GMTowner set
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:3
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:3
<ul>
<li><strong>owner</strong>
set to <em>igloo</em>
</li>
</ul>
<p>
Thanks, I'll add a test.
</p>
TicketsimonpjThu, 14 Oct 2010 07:34:15 GMT
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:4
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:4
<p>
I've noticed that only one of the three errors is reported, at a time. I'll fix that.
</p>
TicketmichaltFri, 15 Oct 2010 18:46:32 GMT
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:5
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:5
<p>
Replying to <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/3651#comment:4" title="Comment 4 for Ticket #3651">simonpj</a>:
</p>
<blockquote class="citation">
<p>
I've noticed that only one of the three errors is reported, at a time. I'll fix that.
</p>
</blockquote>
<p>
You're right! I have absolutely no idea why I've tested them one at a time. Sorry if that caused any confusion.
</p>
TicketiglooSat, 16 Oct 2010 20:59:29 GMTowner changed; testcase set
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:6
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:6
<ul>
<li><strong>owner</strong>
changed from <em>igloo</em> to <em>simonpj</em>
</li>
<li><strong>testcase</strong>
set to <em>T3651</em>
</li>
</ul>
<p>
Test added, but currently fails due to the "only one of the three errors is reported at a time" problem.
</p>
TicketsimonpjTue, 19 Oct 2010 15:56:46 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:7
http://ghc.haskell.org/trac/ghc/ticket/3651#comment:7
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Fixed. We now get all three errors.
</p>
<p>
Simon
</p>
Ticket