<br><font size=3 face="Courier New">Hello,</font>
<br>
<br><font size=3 face="Courier New">I filed the following bug report: </font>
<br>
<br><font size=3 face="Courier New">&nbsp; &nbsp; This produces a type
error: </font>
<br>
<br><font size=3 face="Courier New">&nbsp; &nbsp; &nbsp; &nbsp;foo :: forall
b. (b -&gt; String, Int) &nbsp;</font>
<br><font size=3 face="Courier New">&nbsp; &nbsp; &nbsp; &nbsp;foo = (const
&quot;hi&quot;, 0)</font>
<br><font size=3 face="Courier New">&nbsp; </font>
<br><font size=3 face="Courier New">&nbsp; &nbsp; &nbsp; &nbsp;bar :: (forall
b. b -&gt; String, Int)</font>
<br><font size=3 face="Courier New">&nbsp; &nbsp; &nbsp; &nbsp;bar = foo</font>
<br>
<br><font size=3 face="Courier New">&nbsp; &nbsp; But the types are equivalent.
</font>
<br>
<br><font size=3 face="Courier New">The ticket was closed with a comment
that the types are not equivalent. However, I don't see </font>
<br><font size=3 face="Courier New">how they are not equivalent (in the
presence of impredicative polymorphism) since I can write </font>
<br><font size=3 face="Courier New">derivations for both </font>
<br>
<br><font size=3 face="Courier New">&nbsp; &nbsp; forall b. (b -&gt; String
/\ Int) &nbsp;|- &nbsp;(forall b. b -&gt; String) /\ Int</font>
<br>
<br><font size=3 face="Courier New">and</font>
<br>
<br><font size=3 face="Courier New">&nbsp; &nbsp; (forall b. b -&gt; String)
/\ Int &nbsp;|- &nbsp;forall b. (b -&gt; String /\ Int)</font>
<br>
<br><font size=3 face="Courier New">in intuitionistic logic. </font>
<br>
<br><font size=3 face="Courier New">The counter example given on the bug
tracker is:</font>
<br>
<br><font size=3 face="Courier New">&nbsp; &nbsp; foo :: forall b. (b -&gt;
String, Int)</font>
<br><font size=3 face="Courier New">&nbsp; &nbsp; foo = undefined</font>
<br><font size=3 face="Courier New">&nbsp; &nbsp; </font>
<br><font size=3 face="Courier New">&nbsp; &nbsp; x :: (String, String)</font>
<br><font size=3 face="Courier New">&nbsp; &nbsp; x = case foo of</font>
<br><font size=3 face="Courier New">&nbsp; &nbsp; &nbsp; &nbsp; (f, _)
-&gt; (f 'a', f True)</font>
<br>
<br><font size=3 face="Courier New">which fails to type check where the
other type signature would allow it to check. However, with </font>
<br><font size=3 face="Courier New">impredicative polymorphism, this should
type check.</font>
<br>
<br><font size=3 face="Courier New">Perhaps it is too much to ask the inference
engine to infer the type of f above. However,</font>
<br><font size=3 face="Courier New">in the original code sample, there
is no type inference necessary; it is just necessary to check </font>
<br><font size=3 face="Courier New">if the two types unify, which they
should given the standard interpretation of forall.</font>
<br>
<br><font size=3 face="Courier New">Am I missing something here?</font>
<br>
<br><font size=3 face="Courier New">-Jeff</font>
<br>
<br>
<br>
<span style="font-family:'Arial',sans-serif; font-size:8pt; color:#000000">---<br>
<br>
This e-mail may contain confidential and/or privileged information. If you <br>
are not the intended recipient (or have received this e-mail in error) <br>
please notify the sender immediately and destroy this e-mail. Any <br>
unauthorized copying, disclosure or distribution of the material in this <br>
e-mail is strictly forbidden.</span>