[Haskell-cafe] Impredicativity confusion

[Dimitrios Vytiniotis]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe