<div dir="ltr"><div><div>Hi Iavor,<br><br></div>Thanks for the remarks.<br><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>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&#39;. F a&#39;)`?<br></div><br></div>

-- Conal<br><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki <span dir="ltr">&lt;<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.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 dir="ltr">Hello Conal,<div><br></div><div>The issue with your example is that it is ambiguous, so GHC can&#39;t figure out how to instantiate the use of `foo`.   It might be easier to see why this is if you write it in this form:</div>


<div><br></div><div>&gt; foo :: (F a ~ b) =&gt; b</div><div>&gt; foo = ...</div><div><br></div><div>Now, we can see that only `b` appears on the RHS of the `=&gt;`, so there is really no way for GHC to figure out what is the intended value for `a`.  Replacing `a` with a concrete type (such as `Bool`) eliminates the problem, because now GHC does not need to come up with a value for `a`.   Another way to eliminate the ambiguity would be if `F` was injective---then we&#39;d know that `b` uniquely determines `a` so again there would be no ambiguity.</div>


<div><br></div><div>If `F` is not injective, however, the only workaround would be to write the type in such a way that the function arguments appear in the signature directly (e.g., something like &#39;a -&gt; F a&#39; would be ok).</div>

<span class="HOEnZb"><font color="#888888">
<div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></font></span></div><div class="gmail_extra"><br><br><div class="gmail_quote"><div><div class="h5">


On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott <span dir="ltr">&lt;<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>&gt;</span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div><div class="h5">
<div dir="ltr">I sometimes run into trouble with lack of injectivity for type families. I&#39;m trying to understand what&#39;s at the heart of these difficulties and whether I can avoid them. Also, whether some of the obstacles could be overcome with simple improvements to GHC.<br>




<br>Here&#39;s a simple example:<br><br>&gt; {-# LANGUAGE TypeFamilies #-}<br>&gt;<br>&gt; type family F a<br>&gt;<br>&gt; foo :: F a<br>&gt; foo = undefined<br>&gt;<br>&gt; bar :: F a<br>&gt; bar = foo<br><br>The error message:<br>




<br>    Couldn&#39;t match type `F a&#39; with `F a1&#39;<br>    NB: `F&#39; is a type function, and may not be injective<br>    In the expression: foo<br>    In an equation for `bar&#39;: bar = foo<br><br>A terser (but perhaps subtler) example producing the same error:<br>




<br>&gt; baz :: F a<br>&gt; baz = baz<br><br>Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.<br><br>Does the difficulty here have to do with trying to *infer* the type and then compare with the given one? Or is there an issue even with type *checking* in such cases?<br>




<br>Other insights welcome, as well as suggested work-arounds.<br><br>I know about (injective) data families but don&#39;t want to lose the convenience of type synonym families.<br><br>Thanks,  -- Conal<br><br></div>
<br></div></div><div class="im">_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">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>
<br></div></blockquote></div><br></div>
</blockquote></div><br></div></div>