<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jul 2, 2014 at 7:42 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
2) Suppose one introduces `loopy' by a mistake, and sets its various<br>
invocations, also by a mistake. What can happen then, in the worst case?<br>
Probably, the type checker will loop forever, and the user will<br>
interrupt the process of checking (as I did 10 minutes ago!).<br>
This will not make the whole usage worse, because there are many other<br>
ways in Agda to make the checker loop forever.<br></blockquote><div><br></div><div>There shouldn't be any ways to make the type checker loop forever, so if you have</div><div>any, please report them as bugs. There's a big difference between the type checker</div>
<div>looping and there being inefficiencies in the type checker or your program, making</div><div>checking take a very long time (or run out of memory).</div><div><br></div><div> / Ulf</div></div></div></div>