[Haskell-cafe] Re: Impredicativity confusion
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  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
> 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.
More information about the Haskell-Cafe