[Haskell-cafe] Re: Impredicativity confusion

Gleb Alexeyev gleb.alexeev at gmail.com
Wed Aug 22 10:26:25 EDT 2007

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?


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

More information about the Haskell-Cafe mailing list