<div dir="ltr">Hi,<div><br></div><div>depending on what the plugin does, it is not too hard to get into a loop.  For example, the plugin could keep generating things like:  x > 5, x + 1 > 5, x + 2 > 5, x + 3 > 5.   Of course, this is not a good plan, but one has to be careful to avoid doing it accidentally.   I think that a good general guideline for plugin behavior is like this:</div><div><br></div><div>   - Avoid generating new variables</div><div>   - Only generate constrains of the form: `x = y` or `x = K`: these always make things more defined and could help another solver to make progress</div><div>   - These two ensure that eventually you will run out of new things to generate.</div><div>   - It is occasionally useful to also generate more complex equations:  (e.g. x = y + 1), but then one needs to be careful to ensure progress.</div><div><br></div><div>Despite this, I also don't think that plugins need to be told how many times they've been called: it seems hard for a plugin author to know what to do with this number.  Besides, a buggy plugin could also get stuck in loops in other ways (e.g., get stuck in some internal loop, without going back to GHC).</div><div><br></div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Nov 14, 2014 at 10:09 AM, Eric Seidel <span dir="ltr"><<a href="mailto:eric@seidel.io" target="_blank">eric@seidel.io</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><br>
> On Nov 14, 2014, at 09:14, Adam Gundry <<a href="mailto:adam@well-typed.com">adam@well-typed.com</a>> wrote:<br>
><br>
> Thanks, Simon! I've been convinced that TcS is more than we need, and I<br>
> think the right thing to do is to (optionally) invoke the plugin after<br>
> the constraints have been unflattened anyway. I've just pushed a commit<br>
> to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how<br>
> convenient this alternative is would be most welcome. I'm also wondering<br>
> if the plugin should be told how many times it has been called, to make<br>
> it easier to prevent infinite loops.<br>
<br>
</span>Thanks, I was just sitting down to figure out how to call the plugins<br>
with the unflattened constraints. Is there really a point though in<br>
calling the plugins with flattened and unflattened versions of the same<br>
constraints? Perhaps we should just settle on one or the other? I think<br>
Iavor and I are fine with only passing unflattened constraints to the<br>
plugins. It means a bit more work for the type-nat plugin, but shouldn't<br>
be a huge issue (I'll confirm this before next week).<br>
<br>
I don't think the plugins should be told how often they're being called,<br>
I'd prefer for GHC to track that and break the loop, if anything. I'm<br>
generally unconvinced that tracking the invocations is necessary at all<br>
though. The only way I can see an infinite loop occurring is if the plugins<br>
keep emitting *new* facts. Disregarding the possibility of a malicious<br>
plugin, that should mean that we're making progress towards a solution,<br>
right?<br>
<span class="HOEnZb"><font color="#888888"><br>
Eric<br>
</font></span></blockquote></div><br></div>