<br><br><div class="gmail_quote">On Jan 31, 2008 2:09 AM, Dan Licata <<a href="mailto:drl@cs.cmu.edu">drl@cs.cmu.edu</a>> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Hi everyone,<br><br>Given the usual equality type Id M N and the empty type Void, I'd like<br>to write a function<br><br>contra : Id "nat" "exp" -> Void<br>contra ()<br><br>However, the emptiness checker doesn't notice that this type is<br>
uninhabited (like it would if "nat" and "exp" were two different<br>constructors of a datatype).<br><br>Does anyone know a workaround? Also, would it be hard to catch this<br>case (i.e., treat string literals as constructors), or is this just a<br>
feature that's not implemented yet?</blockquote><div><br>It wouldn't be hard at all. In fact a patch has just been pushed that fixes the issue.<br><br>/ Ulf <br></div></div><br>