Hello,

I filed the following bug report:

    This produces a type error:

       foo :: forall b. (b -> String, Int)  
       foo = (const "hi", 0)
 
       bar :: (forall b. b -> String, Int)
       bar = foo

    But the types are equivalent.

The ticket was closed with a comment that the types are not equivalent. However, I don't see
how they are not equivalent (in the presence of impredicative polymorphism) since I can write
derivations for both

    forall b. (b -> String /\ Int)  |-  (forall b. b -> String) /\ Int

and

    (forall b. b -> String) /\ Int  |-  forall b. (b -> String /\ Int)

in intuitionistic logic.

The counter example given on the bug tracker is:

    foo :: forall b. (b -> String, Int)
    foo = undefined
   
    x :: (String, String)
    x = case foo of
        (f, _) -> (f 'a', f True)

which fails to type check where the other type signature would allow it to check. However, with
impredicative polymorphism, this should type check.

Perhaps it is too much to ask the inference engine to infer the type of f above. However,
in the original code sample, there is no type inference necessary; it is just necessary to check
if the two types unify, which they should given the standard interpretation of forall.

Am I missing something here?

-Jeff


---

This e-mail may contain confidential and/or privileged information. If you
are not the intended recipient (or have received this e-mail in error)
please notify the sender immediately and destroy this e-mail. Any
unauthorized copying, disclosure or distribution of the material in this
e-mail is strictly forbidden.