Typechecker plugins: request for review and another workflow question

Mon Nov 17 15:45:39 UTC 2014

This looks excellent! Thank you Adam and Eric for helping Iavor with this.

But I'm slightly confused by the git history since it seems to be
cluttered with a few merges, and it seems like Eric has pushed the
latest changes to all this. The branch is also a little bit behind
master too.

Iavor, would you like to:

  1) Incorporate all of the changes from Eric and Adam,
  2) Rebase your work on HEAD so we can read it in a digestible way?

I still need to read over all the changes since my first review, since
Adam addressed them. The 7.10 branch is at the end of this week, but
this would be a really cool feature to have.

Thanks!

The branch for 7.10 is now the end of this week! It would be nice to get this in

On Sun, Nov 16, 2014 at 1:33 PM, Eric Seidel <eric at seidel.io> wrote:
> Hi Adam,
>
> I've made a few changes based on your branch. Specifically I've removed
> the call to runTcPlugins inside solveFlats, and have replaced it with
> a specific runTcPluginsGiven that runs in a loop inside solveFlatsGiven
> much like your runTcPluginsFinal runs inside solveFlatsWanted. I think
> this is a bit cleaner given that you've split the wanteds-solving out
> already.
>
> The changes are at https://github.com/gridaphobe/ghc/tree/wip/tc-plugins-els
> since I don't have commit access to GHC :)
>
> Iavor and I also have a question about your change to the last statement
> in solveFlatWanteds. You're putting the unsolved wanteds in a field
> called wc_flat, which suggests that they ought to be flattened. But
> the unsolved wanteds were just unflattened a few lines above! Is this
> a problem, or is the wc_flat field in need of a new name? :)
>
> Eric
>
>
>> 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.
>>
>> I'm very keen to get this into 7.10, appropriately branded as a very
>> experimental feature. Austin, have I sufficiently addressed your
>> concerns about the hs-boot file and multiple flags? Is there anything
>> else we need, apart perhaps from tests and documentation, which I'll put
>> together next week?
>>
>> Thanks,
>>
>> Adam
>>
>>
>> On 12/11/14 11:16, Simon Peyton Jones wrote:
>>> Iavor, Adam, Eric
>>>
>>>
>>>
>>> I’m happy with the general direction of the plugins stuff, so I’m mostly
>>> going to leave it to you guys to plough ahead; but I am happy to respond
>>> to questions.
>>>
>>>
>>>
>>> * 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...
>>>
>>>
>>>
>>> It think the only reason for this is that ‘unflatten’ needs to set
>>> evidence bindings, which in turn requires access to tcs_ev_binds.  I
>>> think that everything else is in TcM.  So I suppose you could carry
>>> around the EvBindsVar if you really didn’t want TcS.  (And I can see why
>>> you wouldn’t; TcS has a lot of stuff you don’t need.)
>>>
>>>
>>>
>>> Simon
>>>
>>>
>>>
>>>
>>>
>>> *From:*Iavor Diatchki [mailto:iavor.diatchki at gmail.com]
>>> *Sent:* 10 November 2014 19:15
>>> *To:* Adam Gundry
>>> *Cc:* ghc-devs at haskell.org; Simon Peyton Jones
>>> *Subject:* Re: Typechecker plugins: request for review and another
>>> workflow question
>>>
>>>
>>>
>>> Hi,
>>>
>>>
>>>
>>> On Mon, Nov 10, 2014 at 1:31 AM, Adam Gundry <adam at well-typed.com
>>> <mailto: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
>>
>>
>> --
>> Adam Gundry, Haskell Consultant
>> Well-Typed LLP, http://www.well-typed.com/
>

-- 
Regards,

Austin Seipp, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/