[Haskell-cafe] Inference for RankNTypes

[Dan Doel]

If you want to know the inner workings, you probably need to read the
OutsideIn(X) paper.*

I'm not that familiar with the algorithm. But what happens is something
like this.... When GHC goes to infer the type of 'f x' where it knows that
f's argument is expected to be polymorphic, this triggers a different code
path that will check that x can be given a type that is at least as general
as is necessary for the argument.

However, "flip one 'x' id" gives flip a type like (alpha -> beta -> gamma)
-> beta -> alpha -> gamma. Then, we probably get some constraints collected
up like:

    alpha ~ (forall a. a -> a)
    alpha ~ (delta -> delta)

That is, it does not compute the higher-rank type of "flip one 'x'" and
then decide how the application of that to id should be checked; it decides
how all the arguments should be checked based only on flip's type, and flip
does not have a higher-rank type on its own. And solving the above
constraints cannot trigger the alternate path.

However, when you factor out or annotate "flip one 'x'", it knows that it's
applying something with a higher-rank type (whether because it inferred it
separately, or you gave it), and that does trigger the alternate code path.

If that's still too vague, you'll have to refer to the paper.

-- Dan

*
http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf


On Wed, Jan 2, 2013 at 11:47 AM, Francesco Mazzoli <f at mazzo.li> wrote:

> At Wed, 2 Jan 2013 11:20:46 -0500,
> Dan Doel wrote:
> > Your example doesn't work for the same reason the following doesn't work:
> >
> >     id runST (<some st code>)
> >
> > It requires the inferencer to instantiate certain variables of id's type
> to
> > polymorphic types based on runST (or flip's based on one), and then use
> > that information to check <some st code> (id in your example) as a
> > polymorphic type. At various times, GHC has had ad-hoc left-to-right
> > behavior that made this work, but it no longer does. Right now, I believe
> > it only has an ad-hoc check to make sure that:
> >
> >     runST $ <some st code>
> >
> > works, and not much else. Note that even left-to-right behavior covers
> all
> > cases, as you might have:
> >
> >     f x y
> >
> > such that y requires x to be checked polymorphically in the same way.
> There
> > are algorithms that can get this right in general, but it's a little
> > tricky, and they're rather different than GHC's algorithm, so I don't
> know
> > whether it's possible to make GHC behave correctly.
> >
> > The reason it works when you factor out or annotate "flip one 'x'" is
> that
> > that is the eventual inferred type of the expression, and then it knows
> to
> > expect the id to be polymorphic. But when it's all at once, we just have
> a
> > chain of unifications relating things like: (forall a. a -> a) ~ beta ~
> > (alpha -> alpha), where beta is part of type checking flip, and alpha ->
> > alpha is the instantiation of id's type with unification variables,
> because
> > we didn't know that it was supposed to be a fully polymorphic use. And
> that
> > unification fails.
>
> Hi Dan,
>
> Thanks a lot for the answer, one forgets that with HM you always replace
> the
> quantified variables immediately.
>
> However I am still confused on how GHC makes it work when I annotate or put
> things in separate variables.  In other words, can you provide links or
> clarify
> how this procedure works:
>
>     The reason it works when you factor out or annotate "flip one 'x'" is
> that
>     that is the eventual inferred type of the expression, and then it
> knows to
>     expect the id to be polymorphic.
>
> Thanks,
> Francesco
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130102/5382fedd/attachment.htm>