<div dir="ltr">Hi Christian,<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">Given &quot;bar :: Bool&quot;, I can&#39;t see how one could go from &quot;Bool&quot; to &quot;F a = Bool&quot; and determine &quot;a&quot; uniquely.<br>

</blockquote><div class="gmail_extra"><br></div><div class="gmail_extra">The same question applies to &quot;foo :: Bool&quot;, right? Yet no error message there.<br><br></div><div class="gmail_extra">Regards, - Conal<br>
</div>
<div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen <span dir="ltr">&lt;<a href="mailto:choener@tbi.univie.ac.at" target="_blank">choener@tbi.univie.ac.at</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br>
<br>
How would you infer &quot;a&quot; from &quot;F a&quot;? Given &quot;bar :: Bool&quot;, I can&#39;t see how<br>
one could go from &quot;Bool&quot; to &quot;F a = Bool&quot; and determine &quot;a&quot; uniquely.<br>
<br>
My question is not completely retorical, if there is an answer I would<br>
like to know it :-)<br>
<br>
Gruss,<br>
Christian<br>
<br>
<br>
* Conal Elliott &lt;<a href="mailto:conal@conal.net">conal@conal.net</a>&gt; [13.01.2013 20:13]:<br>
<div><div class="h5">&gt;    I sometimes run into trouble with lack of injectivity for type families.<br>
&gt;    I&#39;m trying to understand what&#39;s at the heart of these difficulties and<br>
&gt;    whether I can avoid them. Also, whether some of the obstacles could be<br>
&gt;    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 and<br>
&gt;    then compare with the given one? Or is there an issue even with type<br>
&gt;    *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>
&gt;    convenience of type synonym families.<br>
&gt;<br>
&gt;    Thanks,  -- Conal<br>
<br>
</div></div>&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>
</blockquote></div><br></div></div>