<div dir="ltr">Your example doesn't work for the same reason the following doesn't work:<div><br></div><div style> id runST (<some st code>)</div><div style><br></div><div style>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:</div>
<div style><br></div><div style> runST $ <some st code></div><div style><br></div><div style>works, and not much else. Note that even left-to-right behavior covers all cases, as you might have:</div><div style><br>
</div><div style> f x y</div><div style><br></div><div style>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.</div>
<div style><br></div><div style>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.</div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jan 2, 2013 at 8:21 AM, Francesco Mazzoli <span dir="ltr"><<a href="mailto:f@mazzo.li" target="_blank">f@mazzo.li</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
At Wed, 2 Jan 2013 14:49:51 +0200,<br>
<div class="im">Roman Cheplyaka wrote:<br>
> I don't see how this is relevant.<br>
<br>
</div>Well, moving `flip one' in a let solves the problem, and The fact that let-bound<br>
variables are treated differently probably has a play here. I originally<br>
thought that this was because the quantifications will be all to the left in the<br>
let-bound variable while without a let-bound variable the types are used<br>
directly. However this doesn’t explain the behaviour I’m seeing.<br>
<div class="im"><br>
> GHC correctly infers the type of "flip one 'x'":<br>
><br>
> *Main> :t flip one 'x'<br>
> flip one 'x' :: (forall a. a -> a) -> Char<br>
><br>
> But then somehow it fails to apply this to id. And there are no bound<br>
> variables here that we should need to annotate.<br>
<br>
</div>Right. The weirdest thing is that annotating `flip one' (as in `three' in my<br>
code) or indeed `flip one 'x'' with the type that shows up in ghci makes<br>
things work:<br>
<br>
five = (flip one 'x' :: (forall a. a -> a) -> Char) id<br>
<span class="HOEnZb"><font color="#888888"><br>
Francesco<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div>