Re: impredicative type checking

2008-11-11 Thread Jules Bean
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

Re: impredicative type checking

2008-11-11 Thread Chris Kuklewicz
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