<br><div class="gmail_quote">On Fri, Jan 8, 2010 at 11:48 AM, Thorsten Altenkirch <span dir="ltr"><<a href="mailto:txa@cs.nott.ac.uk">txa@cs.nott.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div style="word-wrap:break-word"><div><div class="im"><div>On 8 Jan 2010, at 02:58, Nils Anders Danielsson wrote:</div><blockquote type="cite"><div>I don't think so, but there was some scepticism when injectivity of type<br>
constructors was introduced. See the following thread:<br><br>heterogeneous equality<br><a href="https://lists.chalmers.se/pipermail/agda/2008/000153.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2008/000153.html</a><font color="#000000"><font color="#144FAE"><br>
</font></font></div></blockquote><div><br></div></div>I missed this thread. Interesting, especially Conor's comments.<div class="im"><br><blockquote type="cite"><div>I wanted to see how often I have used this feature, so I reverted the<br>
change Ulf mentions in that thread. It turned out that I only had to<br>modify two functions to make the 168 files of the standard library type<br>check.</div></blockquote><div><br></div></div><div>This is good news.</div>
<div class="im"><br><blockquote type="cite"><div> If reverting this change really is all that is needed to remove<br>automatic type constructor injectivity (Ulf?), then I suggest that we<br>make this feature optional, or remove it entirely.<br>
</div></blockquote><div><br></div></div><div>I'd be in favour to pragmafy it.</div></div></div></blockquote><div><br></div><div>Done. There's now an option --injective-type-constructors which you need to switch on if you want injective type constructors. Without it, Chung's proof doesn't type check. Indeed, there are only two places in the standard libraries which break without the option switched on.</div>
<div><br></div><div>/ Ulf</div></div>