Re: impredicative type checking

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 the type of b becomes fixed. case foo of (f,i) -> {- Here f is monomorphic :: b -> String -} case bar of (f,i) -> {- Here f is still polymorphic :: forall b. b -> String -} Think of how you would seal these with a newtype: newtype Foo = forall a. Foo (a -> String, Int) newtype F = forall a. F (a -> String) type Bar = (F,Int)