Hello,<br><br><div class="gmail_quote">On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones <span dir="ltr">&lt;<a href="mailto:simonpj@microsoft.com">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;    class C a b | a -&gt; b where<br>
| &gt;      foo :: a -&gt; b<br>
| &gt;      foo = error &quot;Yo dawg.&quot;<br>
| &gt;<br>
| &gt;    instance C a b where<br>
|<br>
| The instance &#39;C a b&#39; blatantly violates functional dependency and<br>
| should not have been accepted. The fact that it was is a known bug in<br>
| GHC. The bug keeps getting mentioned on Haskell mailing lists<br>
| about every year. Alas, it is still not fixed. Here is one of the<br>
| earlier messages about it:<br>
|<br>
|   <a href="http://www.haskell.org/pipermail/haskell-cafe/2007-March/023916.html" target="_blank">http://www.haskell.org/pipermail/haskell-cafe/2007-March/023916.html</a><br>
<br>
</div>Wait.  What about<br>
        instance C [a] [b]<br>
?  Should that be accepted?  The Coverage Condition says &quot;no&quot;, and indeed it is rejected. But if you add -XUndecidableInstances it is accepted.<br>
<br>
It&#39;s just the same for<br>
        instance C a b<br>
It is rejected, with the same message, unless you add -XUndecidableInstances.<br>
<br>
Do you think the two are different?  Do you argue for unconditional rejection of everything not satisfying the Coverage Condition, regardless of flags?<br>
<font color="#888888"><br></font></blockquote><div><br></div><div>No, those two are not different, the instance &quot;C [a] [b]&quot; should also be rejected because it violates the functional dependency.  The fact that -XUndecidableInstances accepts this is exactly the bug that keeps being mentioned on the lists every now and then.  The reason that this instance violates the functional dependency is that it allows us to conclude both &quot;C [Int] [Bool]&quot;, and &quot;C [Int] [Char]&quot;, and clearly &quot;[Int] = [Int]&quot;, but &quot;[Bool] /= [Char]&quot;.</div>
<div><br></div><div>The general rule defining an FD on a class like &quot;C&quot; is the following logical statement:</div><div>&quot;forall a b1 b2.  (C a b1, C a b2) =&gt; (b1 = b2)&quot;</div><div><br></div><div>(So I think that the basic concept is really very simple and precise.  I agree that the implementation can be tricky, but a lot of the difficulties are shared with type families---we are just dealing with a hard problem.)</div>
<div><br></div><div>With simple instances (no contexts) it is easy to check if a set of instances is consistent with the FDs of the classes, however when we have conditional instance the task is harder.  This is why we have approximations that ensure consistency (e.g., the Coverage Condition).  My understanding is that the coverage condition in GHC ensures both consistency with the FDs, and termination of the process.  In the past we had another condition,  which ensured consistency but not necessarily termination (I forget its name now but, basically, the rule said that all variables in the target of an FD should be determined from the variables in the source of the FD, but we can use FDs in the context of the instance).   I think the GHC bug is that with -XUndecidableInstances, instances are not validated at all wrt to FDs.  A way to fix that would be to switch to using the old FD validation rule when -XUndecidableInstances are turned on.</div>
<div><br></div><div>-Iavor</div><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><font color="#888888">
Simon<br>
</font><div><div></div><div class="h5"><br>
_______________________________________________<br>
Haskell-prime mailing list<br>
<a href="mailto:Haskell-prime@haskell.org">Haskell-prime@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-prime" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-prime</a><br>
</div></div></blockquote></div><br>