[Haskell-cafe] Re: Impredicativity confusion

[Gleb Alexeyev]

Jeff Polakow wrote:

> boom doesn't typecheck because foo's second argument is of type a which 
> will cause GHC to treat it monomorphically (at least from the top-level 
> of the type-- excuse my ignorance of the correct terminology for this). 
> ok typechecks because the forall is hidden under the A.
> 
I'm sorry, I don't understand this.
GHC manual [1] says that "you can call a polymorphic function at a 
polymorphic type, and parameterise data structures over polymorphic 
types". That's what I do in the code I posted.
What make GHC to treat 'a' monomorphically when explicit type signature 
is given?

[1]http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#impredicative-polymorphism

> To better illustrate, the following will typecheck:
> 
>     foo :: Foo (forall a.a -> a) -> (forall a.a -> a) -> Bool
>     foo = undefined
> 
>     type B = forall a.a -> a
>     boom = foo f (id :: B) where f = undefined :: Foo B
> 
> but this type for foo will prevent ok from typechecking.
> 
> -Jeff
> 
> 
> 
> ---