<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"> This produces a type
error: </font>
<br>
<br><font size=3 face="Courier New"> foo :: forall
b. (b -> String, Int) </font>
<br><font size=3 face="Courier New"> foo = (const
"hi", 0)</font>
<br><font size=3 face="Courier New"> </font>
<br><font size=3 face="Courier New"> bar :: (forall
b. b -> String, Int)</font>
<br><font size=3 face="Courier New"> bar = foo</font>
<br>
<br><font size=3 face="Courier New"> 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"> forall b. (b -> String
/\ Int) |- (forall b. b -> String) /\ Int</font>
<br>
<br><font size=3 face="Courier New">and</font>
<br>
<br><font size=3 face="Courier New"> (forall b. b -> String)
/\ Int |- forall b. (b -> 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"> foo :: forall b. (b ->
String, Int)</font>
<br><font size=3 face="Courier New"> foo = undefined</font>
<br><font size=3 face="Courier New"> </font>
<br><font size=3 face="Courier New"> x :: (String, String)</font>
<br><font size=3 face="Courier New"> x = case foo of</font>
<br><font size=3 face="Courier New"> (f, _)
-> (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>