Hi,

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:

   - Avoid generating new variables
   - 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
   - These two ensure that eventually you will run out of new things to generate.
   - 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.

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).


-Iavor













On Fri, Nov 14, 2014 at 10:09 AM, Eric Seidel <eric@seidel.io> wrote:

> On Nov 14, 2014, at 09:14, Adam Gundry <adam@well-typed.com> wrote:
>
> Thanks, Simon! I've been convinced that TcS is more than we need, and I
> think the right thing to do is to (optionally) invoke the plugin after
> the constraints have been unflattened anyway. I've just pushed a commit
> to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how
> convenient this alternative is would be most welcome. I'm also wondering
> if the plugin should be told how many times it has been called, to make
> it easier to prevent infinite loops.

Thanks, I was just sitting down to figure out how to call the plugins
with the unflattened constraints. Is there really a point though in
calling the plugins with flattened and unflattened versions of the same
constraints? Perhaps we should just settle on one or the other? I think
Iavor and I are fine with only passing unflattened constraints to the
plugins. It means a bit more work for the type-nat plugin, but shouldn't
be a huge issue (I'll confirm this before next week).

I don't think the plugins should be told how often they're being called,
I'd prefer for GHC to track that and break the loop, if anything. I'm
generally unconvinced that tracking the invocations is necessary at all
though. The only way I can see an infinite loop occurring is if the plugins
keep emitting *new* facts. Disregarding the possibility of a malicious
plugin, that should mean that we're making progress towards a solution,
right?

Eric