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.

Hi,

type B = forall a. a->a

boom = foo f (id :: B) where f = undefined :: Foo B

Unfortunately the current implementation of impredicativity has similar problems, which can be summarized as: who gives information (and who should give if any) in application nodes about instantiations of variables; the arguments (and which one?) ? the result types? none? <perhaps-confusing-explanation-skip-if-you-want> Now the source of the particular confusion is that although "Foo B" says that a should be instantiated with "B", the current way applications are checked does not know how to use this information because it is inside a "box". The point is that a "boxy" variable for "a" is filled in (correctly) with B, but then when we are checking: (id :: B) : this_boxy_variable we fail because it is not the case that: forall a. a -> a <= BOX{ forall a. a -> a} Now, there was a good reason for that, boxes represented inferred information that we have no idea *when* they are filled and by who. There are more useful cases for example where we really want: forall a. a -> a <= BOX{ tau -> tau } for any tau. and that is what GHC chooses, and that's what happens algorithmically. </perhaps-confusing-explanation> The whole story of impredicativity in GHC is unsatisfactory; for now you can circumvent your problem by simply providing yourself the correct instantiation of foo: boom = (foo :: Foo B -> B -> Bool) f (id :: B) So, until something is done to fix these issues (I am thinking about it and there exist several related reasearch proposals) a general rule for the current implementation is: give the instantiations yourself if it fails to check. I hope this helps more than confuses, -dimitris

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe