On Tue, Sep 4, 2012 at 11:22 AM, Ian Lynagh <span dir="ltr">&lt;<a href="mailto:ian@well-typed.com" target="_blank">ian@well-typed.com</a>&gt;</span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div id=":1jq">Does anyone think that this check is currently useful, or should I just<br>
turn it off?<br></div></blockquote></div><br><div>I think it should be turned off, or at most become a warning. There&#39;s no particular rhyme or reason to the current naming hierarchy, so freezing it in stone seems arbitrary.</div>