[Haskell-cafe] Inference for RankNTypes
f at mazzo.li
Wed Jan 2 21:02:05 CET 2013
At Wed, 2 Jan 2013 13:35:24 -0500,
Dan Doel wrote:
> 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
Thanks again for the answer. I understood more or less what was going on with
the constraints - what I was wondering is how that alternate code path you cite
works. I guess I’ll have to attack that epic paper sooner or later :).
More information about the Haskell-Cafe