<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv=Content-Type content="text/html; charset=us-ascii">
<meta name=Generator content="Microsoft Word 12 (filtered medium)">
<style>
<!--
/* Font Definitions */
@font-face
        {font-family:Wingdings;
        panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
        {font-family:"Cambria Math";
        panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        margin-bottom:.0001pt;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:purple;
        text-decoration:underline;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
        {mso-style-priority:34;
        margin-top:0cm;
        margin-right:0cm;
        margin-bottom:0cm;
        margin-left:36.0pt;
        margin-bottom:.0001pt;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
span.EmailStyle17
        {mso-style-type:personal-compose;
        font-family:"Calibri","sans-serif";
        color:windowtext;}
.MsoChpDefault
        {mso-style-type:export-only;}
@page WordSection1
        {size:612.0pt 792.0pt;
        margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
        {page:WordSection1;}
/* List Definitions */
@list l0
        {mso-list-id:215361242;
        mso-list-type:hybrid;
        mso-list-template-ids:1951290878 -1476893524 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l0:level1
        {mso-level-start-at:3;
        mso-level-number-format:bullet;
        mso-level-text:\F06E;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:20.4pt;
        text-indent:-18.0pt;
        font-family:Wingdings;
        mso-fareast-font-family:Calibri;
        mso-bidi-font-family:"Times New Roman";}
@list l1
        {mso-list-id:264507450;
        mso-list-type:hybrid;
        mso-list-template-ids:1382838248 -1902344770 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l1:level1
        {mso-level-start-at:3;
        mso-level-number-format:bullet;
        mso-level-text:\F06E;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:22.8pt;
        text-indent:-18.0pt;
        font-family:Wingdings;
        mso-fareast-font-family:Calibri;
        mso-bidi-font-family:"Times New Roman";}
@list l2
        {mso-list-id:928931316;
        mso-list-type:hybrid;
        mso-list-template-ids:-1459083692 986896848 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l2:level1
        {mso-level-start-at:3;
        mso-level-number-format:bullet;
        mso-level-text:\F06E;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:22.8pt;
        text-indent:-18.0pt;
        font-family:Wingdings;
        mso-fareast-font-family:Calibri;
        mso-bidi-font-family:"Times New Roman";}
@list l3
        {mso-list-id:1365642515;
        mso-list-type:hybrid;
        mso-list-template-ids:-378912800 -1349322164 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l3:level1
        {mso-level-start-at:3;
        mso-level-number-format:bullet;
        mso-level-text:\F06E;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        margin-left:20.4pt;
        text-indent:-18.0pt;
        font-family:Wingdings;
        mso-fareast-font-family:Calibri;
        mso-bidi-font-family:"Times New Roman";}
@list l4
        {mso-list-id:2096243981;
        mso-list-type:hybrid;
        mso-list-template-ids:1154107692 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l4:level1
        {mso-level-number-format:bullet;
        mso-level-text:\F0B7;
        mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-18.0pt;
        font-family:Symbol;}
ol
        {margin-bottom:0cm;}
ul
        {margin-bottom:0cm;}
-->
</style>
<!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang=EN-GB link=blue vlink=purple>
<div class=WordSection1>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>Oleg points out, and Martin also mentions, that functional
dependencies appear to interact OK with overlapping instances, but type
families do not. I this impression is mistaken, and I’ll try to explain
why in this message, in the hope of exposing any flaws in my reasoning.<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>We can’t permit overlap for type families because it is <b>unsound
</b>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. <o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>So the short summary of this message is: <b>if it works for
fundeps it works for type families, and vice versa</b>. (NB this
equivalence is not true about GHC’s current implementation, however.
GHC doesn’t support the combination of fundeps and local constraints at
all.)<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>Such an equivalence doesn’t argue against fundeps; I’m
only suggesting the that the two really are very closely equivalent.
I much prefer type families from a programming-style point of view, but that’s
a subjective opinion.<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>Simon<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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:<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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<o:p></o:p></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<o:p></o:p></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)<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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<o:p></o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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.<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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: <o:p></o:p></span></p>
<div style='mso-element:para-border-div;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'><o:p> </o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> class C a b | a -> b<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> data T a where<o:p></o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> import X<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> instance C Int Char where ...<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> f :: Char -> T Int<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> f c = MkT c<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> import X<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> instance C Int Bool<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> g :: T Int -> Bool<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> g (MkT x) = x<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> import M1<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> import M2<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> bad :: Char -> Bool<o:p></o:p></span></p>
<div style='mso-element:para-border-div;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<o:p></o:p></span></p>
</div>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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. <o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> <o:p></o:p></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.<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<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.<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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: <o:p></o:p></span></p>
<div style='mso-element:para-border-div;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'><o:p> </o:p></span></p>
</div>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>{-# LANGUAGE IncoherentInstances #-}<o:p></o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> import X<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> -- Overlapping instances<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> instance C Int Bool --
Instance 1<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> instance C a [a] --
Instance 2<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> f :: Char -> T Int<o:p></o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> g :: T a -> a<o:p></o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> bad :: Char -> Int<o:p></o:p></span></p>
<div style='mso-element:para-border-div;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<o:p></o:p></span></p>
</div>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>Again, a seg fault if it typechecks. But will it? When
typechecking ‘g’, we get a constraint (C a ?), where ‘a’
is a skolem constant. Without IncoherentInstances GHC would reject the
program on the grounds that it does not know what instance to choose. But
*<b>with</b>* IncoherentInstances it would probably go through, which is
unsound. So IncoherentInstances has moved from causing varying dynamic
behaviour to causing seg faults.<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>Very well, so FDL must get rid of IncoherentInstances altogether,
at least for classes that have functional dependencies (or that have superclasses
that do). <o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<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:<o:p></o:p></span></p>
<div style='mso-element:para-border-div;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'><o:p> </o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> -- Overlapping instances<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> instance C Int Bool --
Instance 1<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> instance C a [a] --
Instance 2<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> data T where<o:p></o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> f :: Bool -> T<o:p></o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> g :: T -> T<o:p></o:p></span></p>
<div style='mso-element:para-border-div;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<o:p></o:p></span></p>
<p class=MsoNormal style='border:none;padding:0cm'><span style='font-size:11.0pt;
font-family:"Calibri","sans-serif";color:#1F497D'><o:p> </o:p></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<o:p></o:p></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<o:p></o:p></span></p>
</div>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>In the pattern match for MkT in g we have the constraint (C a
b), where ‘a’ is existentially bound. So under GHC’s
current rules it’ll choose the (C a [a]) instance, and conclude that (b ~
[a]). So it’s ok to reverse x. But it isn’t; see function
bad!<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>So to avoid unsoundness we must not choose a particular instance
from an overlapping set unless we know, absolutely positively, that the other
cases <b>cannot</b> match. <o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>(GHC’s exception for existentials was introduced in
response to user demand. Usually, overlapping instances are somehow semantically
coherent, and with an existential we are *<b>never</b>* going to learn more
about the instantiating type, so choosing the best available seems like a good
thing to do.)<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<div style='mso-element:para-border-div;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:<o:p></o:p></span></p>
</div>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> <b>module</b> M where<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> class C a b | a -> b<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> instance C a [a] --
Instance 2<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> data T where<o:p></o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> g :: T -> T<o:p></o:p></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 <o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></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<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> import M<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> instance C Int Bool --
Instance 1<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'> f :: Bool -> T<o:p></o:p></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<o:p></o:p></span></p>
<div style='mso-element:para-border-div;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'><o:p> </o:p></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<o:p></o:p></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<o:p></o:p></span></p>
</div>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>This is nasty. In module M we have only one instance
declaration for C, so there’s no overlap, and function g typechecks
fine. <o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><br>
Now module Bad adds an overlapping instance declaration and ‘f’ uses
it; moreover, it’s clear that the new instance declaration is the right
one to use.<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>It’s not clear how to fix this. The only way I can
think of is to insist that all the instances appear in a single module, so that
you cannot add more “later”. But that loses part of the point of
overlap in the first place, namely to provide a generic instance and then later
override it.<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>So FDL must <o:p></o:p></span></p>
<p class=MsoListParagraph style='text-indent:-18.0pt;mso-list:l4 level1 lfo1'><![if !supportLists]><span
style='font-size:11.0pt;font-family:Symbol;color:#1F497D'><span
style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>
</span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>embody eager checking for inconsistent instances, across modules<o:p></o:p></span></p>
<p class=MsoListParagraph style='text-indent:-18.0pt;mso-list:l4 level1 lfo1'><![if !supportLists]><span
style='font-size:11.0pt;font-family:Symbol;color:#1F497D'><span
style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>
</span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>never resolve overlap until only a unique instance can possibly
match<o:p></o:p></span></p>
<p class=MsoListParagraph style='text-indent:-18.0pt;mso-list:l4 level1 lfo1'><![if !supportLists]><span
style='font-size:11.0pt;font-family:Symbol;color:#1F497D'><span
style='mso-list:Ignore'>·<span style='font:7.0pt "Times New Roman"'>
</span></span></span><![endif]><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>put all overlapping instances in a single module<o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>Type families already implement the first of these.
I believe that if we added the second and third, then overlap of type families would
be fine. (I may live to eat my words here.) <o:p></o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'><o:p> </o:p></span></p>
<p class=MsoNormal><span style='font-size:11.0pt;font-family:"Calibri","sans-serif";
color:#1F497D'>I’d be interested to know what Chameleon does on these examples.<o:p></o:p></span></p>
</div>
</body>
</html>