[Haskell-cafe] Impredicativity confusion

[Jeff Polakow]

Hello,

> {-# OPTIONS_GHC -fglasgow-exts #-}
> 
> data Foo a
> 
> foo :: Foo a -> a -> Bool
> foo = undefined
> 
> newtype A = A (forall a. a->a)
> 
> ok = foo f (A id)
>      where f = undefined :: Foo A
> 
> type B = forall a. a->a
> 
> boom = foo f (id :: B)
>      where f = undefined :: Foo B
> 
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. 

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




---

This e-mail may contain confidential and/or privileged information. If you 
are not the intended recipient (or have received this e-mail in error) 
please notify the sender immediately and destroy this e-mail. Any 
unauthorized copying, disclosure or distribution of the material in this 
e-mail is strictly forbidden.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070822/513642a1/attachment.htm