Jeff Polakow wrote:
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
Jeff Polakow wrote:
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.
Once you cross the forall