Hello,<br><br><div class="gmail_quote">On Wed, Jul 7, 2010 at 2:14 PM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple">
<div>
<p class="MsoNormal"><span style="color:rgb(31,73,125);font-family:Calibri,sans-serif;font-size:11pt">We can’t permit overlap for type families because it is </span><b style="color:rgb(31,73,125);font-family:Calibri,sans-serif;font-size:11pt">unsound
</b><span style="color:rgb(31,73,125);font-family:Calibri,sans-serif;font-size:11pt">to do so (ie you can break “well typed programs don’t go wrong”).
But if it’s unsound for type families, it would not be surprising if it
was unsound for fundeps too. (I don’t think anyone has done a
soundness proof for fundeps + local constraints + overlapping instances, have
they?) And indeed I think it is. </span></p></div></div></blockquote><div><br></div><div>It would be unsound only if the functional dependencies are not checked properly (which, as you say, is similar to the check for type families). Here is an example of a sound overlap:</div>
<div><br></div><div><font face="courier new, monospace">class C a b | a -> b</font></div><div><font face="courier new, monospace">instance C String Char</font></div><div><font face="courier new, monospace">instance C [a] a</font></div>
<div><br></div><div>Indeed, it would be OK to allow this sort of overlap for type families too, although there it would not be useful, because the more general case already provides the same information as the more specific one. In the case of overlapping instances, the more specific instance might provide a different implementation for the class methods, as usual. (disclaimer: I'm not a fan of overlapping instances----I think that some of the alternative proposals, such as the instance chains work, are nicer, but one would have to do same sort of checks there too).</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"><div lang="EN-GB" link="blue" vlink="purple"><div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> </span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Imagine a system “FDL” that has functional dependencies
and local type constraints. The big deal about this is that you get to exploit
type equalities in *<b>given</b>* constraints. Consider Oleg’s
example, cut down a bit:<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">class C a b | a -> b<u></u><u></u></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">instance C Int Bool<u></u><u></u></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">newtype N2 a = N2 (forall b.
C a b => b)<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">t2 :: N2 Int<u></u><u></u></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">t2 = N2 True<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">We end up type-checking (True :: forall b. C Int b =>
b). From the functional dependency we know that (b~Bool), so the
function should typecheck. GHC rejects this program; FDL would not.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">But making use of these extra equalities in “given”
constraints is quite tricky. To see why look first at Example 1: <u></u><u></u></span></p>
<div style="border:none;border-bottom:double windowtext 2.25pt;padding:0cm 0cm 1.0pt 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
</div>
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">module</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> X where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> class C a b | a -> b<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> data T a where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> MkT :: C a b => b -> T a<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">module</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> M1 where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> import X<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> instance C Int Char where ...<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> f :: Char -> T Int<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> f c = MkT c<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">module</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> M2 where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> import X<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> instance C Int Bool<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> g :: T Int -> Bool<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> g (MkT x) = x<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">module</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> Bad where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> import M1<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> import M2<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> bad :: Char -> Bool<u></u><u></u></span></p>
<div style="border:none;border-bottom:double windowtext 2.25pt;padding:0cm 0cm 1.0pt 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> bad = g . f<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">This program is unsound: it lets you cast an Int to a Bool;
result is a seg-fault. <u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> <u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">You may say that the problem is the inconsistent functional
dependencies in M1 and M2. But GHC won’t spot that. For type
families, to avoid this we “<b>eagerly</b>” check for conflicts in
type-family instances. In this case the conflict would be reported when
compiling module Bad, because that is the first time when both instances are
visible together.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> </span></p></div></div></blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple"><div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">So any FDL system should also make this eager check for
conflicts.</span></p></div></div></blockquote><div><br></div><div>I completely agree with this---we should never allow inconsistent instances to exist in the same scope.</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple"><div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">What about overlap? Here’s Example 2: <u></u><u></u></span></p>
<div style="border:none;border-bottom:double windowtext 2.25pt;padding:0cm 0cm 1.0pt 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">{-# LANGUAGE IncoherentInstances #-}<u></u><u></u></span></p>
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">module</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> Bad where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> import X<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> -- Overlapping instances<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> instance C Int Bool --
Instance 1<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> instance C a [a] --
Instance 2<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> f :: Char -> T Int<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> f c = MkT c --
Uses Instance 1<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> g :: T a -> a<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> g (MkT x) = x --
Uses Instance 2<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> bad :: Char -> Int<u></u><u></u></span></p>
<div style="border:none;border-bottom:double windowtext 2.25pt;padding:0cm 0cm 1.0pt 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> bad = g . f<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> </span></p></div></div></blockquote><div><br></div><div>As in the above example, this program violates the functional dependency on class C and should be rejected, because the two instances are not consistent with each other.</div>
<div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div lang="EN-GB" link="blue" vlink="purple"><div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">But at the moment GHC makes an exception for *<b>existentials</b>*.
Consider Example 3:<u></u><u></u></span></p>
<div style="border:none;border-bottom:double windowtext 2.25pt;padding:0cm 0cm 1.0pt 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> class C a b | a -> b<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> -- Overlapping instances<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> instance C Int Bool --
Instance 1<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> instance C a [a] --
Instance 2<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> data T where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> MkT :: C a b => a -> b -> T<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> f :: Bool -> T<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> f x = MkT (3::Int) x --
Uses Instance 1<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> g :: T -> T<u></u><u></u></span></p>
<div style="border:none;border-bottom:double windowtext 2.25pt;padding:0cm 0cm 1.0pt 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> g (MkT n x) = MkT n
(reverse x) -- Uses Instance 2<u></u><u></u></span></p>
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> bad :: Bool -> T<u></u><u></u></span></p>
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> bad = g . f<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"></span></p></div></div></blockquote><div>This program is malformed for the same reason as the previous one: the two instances violate the functional dependency on the class.</div>
<div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div lang="EN-GB" link="blue" vlink="purple"><div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div style="border:none;border-bottom:double windowtext 2.25pt;padding:0cm 0cm 1.0pt 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">But even nuking
IncoherentInstances altogether is not enough. Consider this variant of
Example 3, call it Example 4:<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> <b>module</b> M where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> class C a b | a -> b<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> instance C a [a] --
Instance 2<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> data T where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> MkT :: C a b => a -> b -> T<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> g :: T -> T<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> g (MkT n x) = MkT n (reverse x) -- Uses Instance
2 <u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">module</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> Bad where<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> import M<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> instance C Int Bool --
Instance 1<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> f :: Bool -> T<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> f x = MkT (3::Int) x --
Uses Instance 1<u></u><u></u></span></p>
<div style="border:none;border-bottom:double windowtext 2.25pt;padding:0cm 0cm 1.0pt 0cm">
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> bad :: Bool -> T<u></u><u></u></span></p>
<p class="MsoNormal" style="border:none;padding:0cm"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> bad = g . f<u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"></span></p></div></div></blockquote><div><br></div><div>We must be thinking about these examples in a rather different way :-) Like the others, I'd say that this program should be rejected because it violates the functional dependency on the class and should be rejected.</div>
<div><br></div><div>The way I think of a functional dependency on a class is that it restricts what instances are allowed to co-exist in the same scope. So GHC needs to ensure that its instance database never contains instances that violate the functional dependency property. This amounts to three checks:</div>
<div><br></div><div>1. Check that an instance is consistent with itself. For example, this should be rejected:</div><div><br></div><div><font face="courier new, monospace">instance C a b</font></div><div><br></div><div>because it allows <font face="courier new, monospace">C Int Bool</font> and <font face="courier new, monospace">C Int Char </font><font face="arial, helvetica, sans-serif">which violate the functional dependency.</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">2. Check that an instance is consistent with all other instances in scope. Note that this is orthogonal to the overlapping check: instances need to be consistent with the fun. dep. independent of overlap.</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">3. Check that instances imported from different modules are consistent with each other. This is really a special case of 2, and GHC must already be doing some checking at this point to avoid duplicated instances.</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">It is important that the checks for consistency are sound. They are not likely to be complete (i.e., we might reject some programs that do not really violate the fun.dep. but GHC can't see it),</font></div>
<div><font face="arial, helvetica, sans-serif">but that's OK. The usual rule, I forget its name, falls in this category.</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">Finally for the payoff of all this: because we know that GHC is going to enforce the fun. dep. invariant, we can use it when we type check things. For example, consider the standard example:</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">f :: (C a b, C a c) => a -> b -> c</font></div><div><font face="arial, helvetica, sans-serif">f x y = y</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">This is OK, but only as long as GHC ensures that all instances of C satisfy the fun. dep. invariant. If the invariant is satisfied, however, then we know that whenever "f" is used, the instances that will be used to discharge its constraints are going the satisfy the fun. dep. and so "b" and "c" will be the same.</font></div>
<div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">-Iavor</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif"><br>
</font></div><div><br></div></div>