Typechecker plugins: request for review and another workflow question

[Iavor Diatchki]

Hi,

On Mon, Nov 10, 2014 at 1:31 AM, Adam Gundry <adam at well-typed.com> wrote:

>
> On the subject of that "nearly", I'm interested to learn whether you
> have a suggestion to deal with unflattening, because the interface still
> works with flat constraints only. Simon's changes should make it more
> practical to unflatten inside the plugin, but it would be far easier (at
> least for my purposes) if it was simply given unflattened constraints. I
> realise that this would require the plugin loop to be pushed further
> out, however, which has other difficulties.
>

Not sure what to do about this.  With the current setup, I think either
way, the plugin would have to do some extract work.   Perhaps we should run
the plugins on the unflattened constraints, and leave to the plugins to
manually temporarily "flatten" terms from external theories?  For example,
if the type-nat plugin saw `2 * F a ~ 4`, it could temporarily work with `2
* x ~ 4`, and then when it figures out that `x ~ 2`, it could emit `F a ~
2` (non-canonical), which would go around again, and hopefully get fully
simplified.



> A few other issues, of lesser importance:
>
>  * I still think it would be better to provide an escape hatch to the
> TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably,
> Simon's new TcFlatten.unflatten needs TcS...
>
> I don't mind that but, if I recall correctly, to do this without more
recursive modules, we had to split `TCSMonad` in two parts, one with the
types, and one with other stuff.  Eric and I did this once, but we didn't
commit it, because it seemed like an orthogonal change.



>  * Is there a way for my plugin to "solve" a given constraint (e.g. to
> discard the uninformative "a * 1 ~ a")?
>
> Yes, you'd say something like: `TcPluginOK [(evidence, "a * 1 ~ a")] []`

The first field of `TcPluginOK` are things that are solved, the second one
is new work.


>  * It is unfortunately easy to create infinite loops by writing plugins
> that emit wanteds but make no useful progress. Perhaps there should be a
> limit on the number of times round the loop (like SubGoalDepth but for
> all constraints)?
>
>
Indeed, if a plugin keeps generating new work, we could go in a loop, so
maybe a limit of some sort is useful.  However, note that if the plugin
generates things that are already in the inert set, GHC should notice this
and filter them, so we won't keep going.



>  * Perhaps runTcPlugin should skip invoking the plugin if there are no
> wanteds?
>

Oh, there is an important detail here that needs documentation!   GHC will
call the plugin twice: once to improve the givens, and once to solve the
wanteds.   The way to distinguish the two is exactly by the presence of the
wanteds.

Why might you want to improve the givens?  Suppose you had something like
`x * 2 ~ 4` as a given:  then you'd really want the plugin to generate
another given: `x ~ 2`, as this is likely to help the rest of the
constraint solving process.


>  * The use of ctev_evar in runTcPlugin is partial, and fails with a
> nasty error if the plugin returns a non-wanted in the solved constraints
> list. Would it be worth catching this error and issuing a sensible
> message that chastises the plugin author appropriately?
>

Aha, good idea. Bad plugin! :-)


 * Finally, I presume the comment on runTcPlugin that "The plugin is
> provided only with CTyEq and CFunEq constraints" is simply outdated and
> should be removed?
>
> Yep, thanks!


> Apologies for the deluge of questions - please take them as evidence of
> my eagerness to use this feature!
>

Thanks for your feedback!  Also, if you feel like doing some hacking please
do so---I am quite busy at the moment so I don't  have a ton of time to
work on it, so any help you be most appreciated.  I know Eric is also quite
keen on helping out so we can just coordinate over e-mail.

-Iavor
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20141110/217bd44c/attachment-0001.html>