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.