Re: Typechecker plugins: request for review and another workflow question

Indeed, I spoke too soon. The type-nat plugin in fact causes an infinite loop when run on the unflattened constraints for one of our examples.. I think it would be reasonable for TcM to track how many times it has called the plugins and disable them after N iterations. But I don't know what would be a sensible default for N :/

On Nov 14, 2014, at 10:50, Iavor Diatchki wrote:

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 wrote:

...

On Nov 14, 2014, at 09:14, Adam Gundry 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