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._______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
