
<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div>On 8 Jan 2010, at 02:58, Nils Anders Danielsson wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>On 2010-01-07 11:30, Thorsten Altenkirch wrote:<br><blockquote type="cite">congratulations! I didn't know about this problem and I think it is a<br></blockquote><blockquote type="cite">serious issue indeed.<br></blockquote><br>I agree.<br><br><blockquote type="cite">Maybe it is a known issue? Nisse? Ulf?<br></blockquote><br>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">https://lists.chalmers.se/pipermail/agda/2008/000153.html</a><font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div>I missed this thread. Interesting, especially Conor's comments.<br><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>This is good news.</div><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>I'd be in favour to pragmafy it.</div><div><br></div><div>Cheers,</div><div>Thorsten</div></div></body></html>