&gt; I expected the type of &#39;x&#39; to be universally quantified, and thus can be<br>&gt; unified with &#39;forall a. a&#39; with no problem<br><br>As I get it. &#39;x&#39; is not universally quantified. f is. [1]<br>x would be universally quantified if the type of f was :<br>


<br>f :: (forall a. a) -&gt; (forall a. a)<br><br>[1] Yet here I&#39;m not sure this sentence is correct. Some heads-up from a type expert would be good.<br><br><br>Would you try:<br><br>f :: a -&gt; a<br>f x = undefined :: a<br>

<br>And tell me if it works? IMO it doesn&#39;t.<br><br><div class="gmail_quote">2012/1/4 Yucheng Zhang <span dir="ltr">&lt;<a href="mailto:yczhang89@gmail.com" target="_blank">yczhang89@gmail.com</a>&gt;</span><br>
<blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>On Wed, Jan 4, 2012 at 7:58 PM, Yves Parès &lt;<a href="mailto:limestrael@gmail.com" target="_blank">limestrael@gmail.com</a>&gt; wrote:<br>



&gt; f :: forall a. a -&gt; a<br>
&gt; f x = x :: forall a. a<br>
&gt;<br>
&gt; Which is obviously wrong: when you have entered f, x has been instatiated to<br>
&gt; a specific type &#39;a&#39;, and then you want it to x to be of any type? That<br>
&gt; doesn&#39;t make sense.<br>
<br>
</div>I did not expect the type variables to be scoped.<br>
<br>
I expected the type of &#39;x&#39; to be universally quantified, and thus can be unified<br>
with &#39;forall a. a&#39; with no problem.<br>
</blockquote></div><br>