GHC: Ticket #6075: Incorrect interpretation of scoped type variable declaration in GADT pattern match
http://ghc.haskell.org/trac/ghc/ticket/6075
<p>
Consider the following code:
</p>
<pre class="wiki">{-# LANGUAGE GADTs, FlexibleInstances, ScopedTypeVariables #-}
class FromThinAir a where
create :: a
instance FromThinAir Int where
create = 42
instance FromThinAir [Char] where
create = "Poof!"
data GADT a where
GInt :: GADT Int
GArrow :: (FromThinAir a, Show a) => GADT (a -> b)
data NotGADT where
NInt :: Int -> NotGADT
NArrow :: (FromThinAir a, Show a) => (a -> b) -> NotGADT
dumb :: NotGADT -> String
dumb g = case g of
NInt _ -> show (create :: Int)
NArrow (f :: (a -> b)) -> show (create :: a)
dumber :: GADT a -> String
dumber g = case g of
GInt -> show (create :: Int)
(GArrow :: GADT (a -> b)) -> show (create :: a)
</pre><p>
The function <tt>dumb</tt> compiles just fine. The function <tt>dumber</tt> does not. The problem appears to be that GHC interprets the type signature on <tt>GArrow</tt> as a type signature that applies to all cases, or (equivalently) applies to <tt>g</tt>. In <tt>dumb</tt>, however, the type signature is applied to a variable, not the constructor, and GHC does the right thing.
</p>
<p>
Note that the <tt>FromThinAir</tt> class simply sets the stage for the bug. I don't believe it's an integral part of it all.
</p>
<p>
This was tested on 7.5.20120426.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/6075
Trac 1.0.1simonpjSat, 05 May 2012 12:05:54 GMTstatus changed; difficulty, resolution set
http://ghc.haskell.org/trac/ghc/ticket/6075#comment:1
http://ghc.haskell.org/trac/ghc/ticket/6075#comment:1
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>resolution</strong>
set to <em>invalid</em>
</li>
</ul>
<p>
The errror mesage (with GHC 7.4) is this:
</p>
<pre class="wiki">T6075.hs:27:3:
Couldn't match type `a -> b' with `Int'
Inaccessible code in
a pattern with constructor GInt :: GADT Int, in a case alternative
In the pattern: GInt
In a case alternative: GInt -> show (create :: Int)
</pre><p>
And that seems right to me. Consider the <a class="ext-link" href="http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.17"><span class="icon"></span>semantics of pattern matching in the Haskell report</a>. To 3.17.2 add the informal rule
</p>
<ul><li>Matching the pattern <tt>(p :: ty)</tt> against a value <tt>v</tt> requires <tt>v</tt> to have type <tt>ty</tt> (or else a static error results), and then matches <tt>p</tt> against <tt>v</tt>.
</li></ul><p>
To 3.17.3 add a rule for type signatures
</p>
<pre class="wiki">case v of { (p :: type) -> e1; _ -> e2 }
=
case (v :: type) of { p -> e1; _ -> e2 }
</pre><p>
(This rule does not take account of bringing lexical type variables into scope, but is otherwise right.)
</p>
<p>
In short, patterns are matched outside in, so we don't get to see that the pattern has type <tt>GADT (a->b)</tt> until <em>after</em> we've matched <tt>GArrow</tt>, but the type signature applies <em>before</em>.
</p>
Ticket