<div dir="ltr">Hi,<div><br></div><div>that's an interesting example.  To me this looks like a bug in GHC, although the issue is certainly a bit subtle.</div><div><br></div><div>The reason I think it is a bug is that, if we name all the type functions in the signature and apply improvements using the fact that we are working with functions, then we get:</div><div><br></div><div>    x :: (F a ~ b, G b ~ a) => b</div><div>    x = undefined</div><div><br></div><div>Now, this should be equivalent, and it is quite clear that there is no ambiguity here, as the `b` determines the `a` via the `G`.   Interestingly, GHC accepts the program in this form.  Also, if you ask it for the type of `x` using `:t` (which means instantiate the type and the generalize it again), we get another equivalent formulation: `x :: (F (G b) ~ b) => b`, which is also accepted by GHC. </div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 2, 2015 at 9:28 AM, Wolfgang Jeltsch <span dir="ltr"><<a href="mailto:g9ks157k@acme.softbase.org" target="_blank">g9ks157k@acme.softbase.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
the following (contrived) code is accepted by GHC 7.8.3, but not 7.10.1:<br>
<br>
> {-# LANGUAGE TypeFamilies #-}<br>
><br>
> type family F a :: *<br>
><br>
> type family G b :: *<br>
><br>
> x :: G (F a) ~ a => F a<br>
> x = undefined<br>
<br>
GHC 7.10.1 reports:<br>
<br>
> Could not deduce (F a0 ~ F a)<br>
> from the context (G (F a) ~ a)<br>
>   bound by the type signature for x :: (G (F a) ~ a) => F a<br>
>   at Test.hs:7:6-23<br>
> NB: ‘F’ is a type function, and may not be injective<br>
> The type variable ‘a0’ is ambiguous<br>
> In the ambiguity check for the type signature for ‘x’:<br>
>   x :: forall a. (G (F a) ~ a) => F a<br>
> To defer the ambiguity check to use sites, enable AllowAmbiguousTypes<br>
> In the type signature for ‘x’: x :: G (F a) ~ a => F a<br>
<br>
At a first look, this complaint seems reasonable, and I have already<br>
wondered why GHC 7.8.3 actually accepts the above code.<br>
<br>
>From an intuitive standpoint, however, the code seems actually<br>
acceptable to me. While it is true that type families are generally not<br>
injective, it is possible to derive the type a from F a by applying G.<br>
<br>
It would great if this code would be accepted by GHC again and if there<br>
was a workaround to make it work with GHC 7.10.1. At the moment, this<br>
change in the type checker from 7.8.3 to 7.10.1 breaks the<br>
incremental-computing package in a rather fundamental way.<br>
<br>
All the best,<br>
Wolfgang<br>
<br>
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users</a><br>
</blockquote></div><br></div>