<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 15 (filtered medium)"><style><!--
/* Font Definitions */
@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:11.0pt;
font-family:"Calibri","sans-serif";
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri","sans-serif";
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri","sans-serif";
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></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="#0563C1" vlink="#954F72"><div class=WordSection1><p class=MsoNormal>(Sorry for the re-send – got the wrong subject line last time.)<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Hello all,<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>It’s come to my attention that there is a tiny lurking potential hole in GHC’s type safety around type families in the presence of UndecidableInstances. Consider the following:<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>> type family F a b<o:p></o:p></p><p class=MsoNormal>> type instance F x x = Int<o:p></o:p></p><p class=MsoNormal>> type instance F [x] x = Bool<o:p></o:p></p><p class=MsoNormal>><o:p> </o:p></p><p class=MsoNormal>> type family G<o:p></o:p></p><p class=MsoNormal>> type family G = [G]<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>This declarations are all valid in GHC 7.6.3. However, depending on the reduction strategy used, it is possible to reduce `F G G` to either Int or Bool. I haven’t been able to get this problem to cause a seg-fault in practice, but I think that’s more due to type families’ strictness than anything more fundamental. Thus, we need to do something about it.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>I have written a proposal on the GHC wiki at <a href="http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/Nonlinearity">http://hackage.haskell.org/trac/ghc/wiki/NewAxioms/Nonlinearity</a><o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>It proposes a change to the syntax for branched instances (a new form of type family instance that allows for ordered matching), but as those haven’t yet been officially released (only available in HEAD), I’m not too worried about it.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>There are two changes, though, that break code that compiles in released versions of GHC:<o:p></o:p></p><p class=MsoNormal>---<o:p></o:p></p><p class=MsoNormal>1) Type family instances like the two for F, above, would no longer be accepted. In particular, the overlap check for unbranched (regular standalone instances like we’ve had for years) would now check for overlap if all variables were distinct. (This freshening of variables is called ‘linearization’.) Thus, the check for F would look at `F x y` and `F [x] y`, which clearly overlap and would be conflicting.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>2) Coincident overlap between unbranched instances would now be prohibited. In the new version of GHC, these uses of coincident overlap would have to be grouped in a branched instance. This would mean that all equations that participate in coincident overlap would have be defined in the same module. Cross-module uses of coincident overlap may be hard to refactor.<o:p></o:p></p><p class=MsoNormal>---<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Breaking change #1 is quite necessary, as that’s the part that closes the hole in the type system.<o:p></o:p></p><p class=MsoNormal>Breaking change #2 is strongly encouraged by the fix to #1, as the right-hand side of an instance is ill-defined after the left-hand side is linearized. It is conceivable that there is some way to recover coincident overlap on unbranched instances, but it’s not obvious at the moment. Note that this proposal does not contain a migration path surrounding coincident overlap. In GHC <= 7.6.x, branched instances don’t exist and we have coincident overlap among unbranched instances; and in GHC >= 7.8.x, we will prohibit coincident overlap except within branched instances. We (Simon PJ and I) think that this shouldn’t be too big of a problem, but please do shout if it would affect you.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Please let me know what you think about this proposal!<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Thanks,<o:p></o:p></p><p class=MsoNormal>Richard<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p></div></body></html>