<div dir="ltr">Hello,<div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott <span dir="ltr"><<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>></span> wrote:<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><div><div class="im"><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">so there is really no way for GHC to figure out what is the intended value for `a`.<br>
</blockquote><div><br></div></div><div>Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`?</div></div>
</div></blockquote><div><br></div><div style>Wouldn't that make `F` a constant type family, and so one could just skip the `a` parameter? Anyway, if there was a way to assert something like that about a type-function, than there would be no problem. When something like that happens (i.e., GHC figures out that it does not know how to instantiate a type variable, but it is sure that the actual instantiation does not matter), GHC instantiates the variable a special type called `Any`, which has a very polymorphic kind.</div>
<div style><br></div><div style>By the way, Simon recently reworked the ambiguity checker in GHC, and now HEAD correctly rejects `foo` as being ambiguous (the new ambiguity check uses exactly what's in your example: a value `f :: S` is ambiguous, if `g :: S; g = f` results in an error).<br>
</div><div style><br></div><div style>-Iavor</div><div><br></div><div> </div></div><br></div></div>