Typechecker plugins: request for review and another workflow question

[Iavor Diatchki]

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 at seidel.io> wrote:

>
> > On Nov 14, 2014, at 09:14, Adam Gundry <adam at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20141114/0817543b/attachment.html>