GHC: Ticket #5650: Type error when annotating a let binding with a forall type
http://ghc.haskell.org/trac/ghc/ticket/5650
<p>
I'm not sure if this is a bug or not, but it's certainly counterintuitive to me.
</p>
<p>
Why does this example fail to type check?
</p>
<pre class="wiki">Prelude> let (x :: forall a. a -> a) = id in x 3
<interactive>:0:31:
Couldn't match expected type `forall a. a -> a'
with actual type `a0 -> a0'
In the expression: id
In a pattern binding: (x :: forall a. a -> a) = id
</pre><p>
I have <code>RankNTypes</code> and <code>ScopedTypeVariables</code> enabled.
</p>
<p>
I asked this question on StackOverflow: <a class="ext-link" href="http://stackoverflow.com/questions/8190431/type-error-when-ascribing-a-valid-forall-type-to-a-let-bound-variable"><span class="icon"></span>http://stackoverflow.com/questions/8190431/type-error-when-ascribing-a-valid-forall-type-to-a-let-bound-variable</a>
</p>
<p>
User ibid's theory there was this:
</p>
<p>
"In a let binding let x = id in ..., what happens is that id's type forall a. a->a gets instantiated into a monotype, say a0 -> a0, which is then assigned as x's type and is then generalized as forall a0. a0 -> a0. If, as I think, the pattern type signature is checked before generalization, it's essentially asking the compiler to verify that the monotype a0 -> a0 is more general than the polytype forall a. a -> a, which it isn't."
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/5650
Trac 1.2iglooWed, 23 Nov 2011 20:53:01 GMTowner, milestone set
http://ghc.haskell.org/trac/ghc/ticket/5650#comment:1
http://ghc.haskell.org/trac/ghc/ticket/5650#comment:1
<ul>
<li><strong>owner</strong>
set to <em>simonpj</em>
</li>
<li><strong>milestone</strong>
set to <em>7.4.1</em>
</li>
</ul>
TicketpelotomThu, 01 Dec 2011 05:07:04 GMT
http://ghc.haskell.org/trac/ghc/ticket/5650#comment:2
http://ghc.haskell.org/trac/ghc/ticket/5650#comment:2
<p>
I also asked <a class="ext-link" href="http://stackoverflow.com/questions/7657827/fun-with-impredicative-polymorphism-and-type-ascription"><span class="icon"></span>this question on SO</a>, which seems like it may be a related. In that case, GHC 6.12.1 actually accepts the type, whereas 7.x rejects it.
</p>
TicketsimonpjTue, 13 Dec 2011 16:08:16 GMTstatus changed; difficulty, resolution set
http://ghc.haskell.org/trac/ghc/ticket/5650#comment:3
http://ghc.haskell.org/trac/ghc/ticket/5650#comment:3
<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>
It's quite right actually. The Haskell 2010 Report, in the section on pattern bindings, <a class="ext-link" href="http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-880004.5"><span class="icon"></span>http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-880004.5</a>, defines the static semantics of
</p>
<pre class="wiki"> p = e
</pre><p>
where pattern <code>p</code> binds variables <code>x1</code> .. <code>xn</code>, thus:
</p>
<pre class="wiki"> t = e
x1 = case t of p -> x1
...
xn = case t of p -> xn
</pre><p>
So let's try that with your example, which is a (degenerate) pattern binding:
</p>
<pre class="wiki"> t = id
x = case t of (x :: forall a. a->a) -> x
</pre><p>
When you typecheck this, <code>t</code> gets type <code>forall a. a->a</code>, but the <em>occurrence</em> of <code>t</code> in the rhs of <code>x</code> is instantiated, of course, to give type <code>b -> b</code>, where we don't yet know the type <code>b</code>. And that fails to match the type of x in the pattern.
</p>
<p>
So I think GHC is following the specification.
</p>
<p>
Simon
</p>
Ticket