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 <iavor.diatc...@gmail.com> 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 <e...@seidel.io> wrote: > > > On Nov 14, 2014, at 09:14, Adam Gundry <a...@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 > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
