<div dir="ltr"><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">There is a real difficulty here with type-checking &#39;bar&#39;.  (And that difficulty is why &#39;foo&#39; is also rejected.)</blockquote>

<div><br></div><div>Oh! Is the definition of &#39;foo&#39; rejected in recent versions of GHC? My 7.4.1 installation doesn&#39;t complain.   -- Conal<br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">

On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones <span dir="ltr">&lt;<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div class="im">| &gt; &gt; {-# LANGUAGE TypeFamilies #-}<br>
| &gt; &gt;<br>
| &gt; &gt; type family F a<br>
| &gt; &gt;<br>
| &gt; &gt; foo :: F a<br>
| &gt; &gt; foo = undefined<br>
| &gt; &gt;<br>
| &gt; &gt; bar :: F a<br>
| &gt; &gt; bar = foo<br>
<br>
</div>There is a real difficulty here with type-checking &#39;bar&#39;.  (And that difficulty is why &#39;foo&#39; is also rejected.)<br>
<br>
Namely, when typechecking &#39;bar&#39;, we must instantiate foo with an unknown type, say alpha.  So now we must find a type &#39;alpha&#39; such that<br>
        F a ~ F alpha<br>
Certainly alpha=1 is one solution, but there might be others.  For example, suppose<br>
        type instance F [b] = F b<br>
Then alpha=[a] would also be a solution.<br>
<br>
In this particular case any solution will do, but suppose there was an addition constraint (C alpha) arising from the right hand side, where C is a class.  Then if we had<br>
        instance C [b] where ...<br>
then the second solution (alpha=[a]) would work, but not the first.  This can get arbitrarily complicated, and GHC&#39;s type inference does not &quot;search&quot; various solutions; it follows one path.<br>
<br>
The solution is to provide a way to fix alpha. For example,<br>
        foo :: a -&gt; F a<br>
is fine.<br>
<span class="HOEnZb"><font color="#888888"><br>
Simon<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
| -----Original Message-----<br>
| From: <a href="mailto:glasgow-haskell-users-bounces@haskell.org">glasgow-haskell-users-bounces@haskell.org</a> [mailto:<a href="mailto:glasgow-haskell-">glasgow-haskell-</a><br>
| <a href="mailto:users-bounces@haskell.org">users-bounces@haskell.org</a>] On Behalf Of Richard Eisenberg<br>
| Sent: 14 January 2013 03:47<br>
| To: Conal Elliott<br>
| Cc: <a href="mailto:glasgow-haskell-users@haskell.org">glasgow-haskell-users@haskell.org</a>; Haskell Cafe<br>
| Subject: Re: Advice on type families and non-injectivity?<br>
|<br>
| Hi Conal,<br>
|<br>
| I agree that your initial example is a little puzzling, and I&#39;m glad<br>
| that the new ambiguity checker prevents both definitions, not just one.<br>
|<br>
| However, your initial question seems broader than just this example. I<br>
| have run into this problem (wanting injective type functions) several<br>
| times myself, and have been successful at finding workarounds. But, I<br>
| can&#39;t think of any unifying principle or solid advice. If you can post<br>
| more information about your problem, perhaps I or others can contribute.<br>
|<br>
| For what it&#39;s worth, the desire for injective type functions has been<br>
| entered as ticket #6018 in the GHC Trac, but I see you&#39;re already on the<br>
| cc: list. I believe Simon PJ has given serious thought to implementing<br>
| this feature and may have even put in some very basic code toward this<br>
| end.<br>
|<br>
| Richard<br>
|<br>
| On Jan 13, 2013, at 2:10 PM, Conal Elliott &lt;<a href="mailto:conal@conal.net">conal@conal.net</a>&gt; wrote:<br>
|<br>
| &gt; I sometimes run into trouble with lack of injectivity for type<br>
| families. I&#39;m trying to understand what&#39;s at the heart of these<br>
| difficulties and whether I can avoid them. Also, whether some of the<br>
| obstacles could be overcome with simple improvements to GHC.<br>
| &gt;<br>
| &gt; Here&#39;s a simple example:<br>
| &gt;<br>
| &gt; &gt; {-# LANGUAGE TypeFamilies #-}<br>
| &gt; &gt;<br>
| &gt; &gt; type family F a<br>
| &gt; &gt;<br>
| &gt; &gt; foo :: F a<br>
| &gt; &gt; foo = undefined<br>
| &gt; &gt;<br>
| &gt; &gt; bar :: F a<br>
| &gt; &gt; bar = foo<br>
| &gt;<br>
| &gt; The error message:<br>
| &gt;<br>
| &gt;     Couldn&#39;t match type `F a&#39; with `F a1&#39;<br>
| &gt;     NB: `F&#39; is a type function, and may not be injective<br>
| &gt;     In the expression: foo<br>
| &gt;     In an equation for `bar&#39;: bar = foo<br>
| &gt;<br>
| &gt; A terser (but perhaps subtler) example producing the same error:<br>
| &gt;<br>
| &gt; &gt; baz :: F a<br>
| &gt; &gt; baz = baz<br>
| &gt;<br>
| &gt; Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.<br>
| &gt;<br>
| &gt; Does the difficulty here have to do with trying to *infer* the type<br>
| and then compare with the given one? Or is there an issue even with type<br>
| *checking* in such cases?<br>
| &gt;<br>
| &gt; Other insights welcome, as well as suggested work-arounds.<br>
| &gt;<br>
| &gt; I know about (injective) data families but don&#39;t want to lose the<br>
| convenience of type synonym families.<br>
| &gt;<br>
| &gt; Thanks,  -- Conal<br>
| &gt;<br>
| &gt; _______________________________________________<br>
| &gt; Glasgow-haskell-users mailing list<br>
| &gt; <a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
| &gt; <a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
|<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://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
</div></div></blockquote></div><br></div>