impredicative type checking

[Jeff Polakow]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081110/f3d0c25c/attachment.htm