impredicative type checking

[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 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)