Typechecker plugins: request for review and another workflow question

Austin Seipp austin at well-typed.com
Mon Nov 17 15:59:38 UTC 2014 

Yes, that would be ideal, and it can built/test it for you.

This is all enough for one patch I imagine, which should be pretty
easy to rebase locally, then submit with `arc diff`.

On Mon, Nov 17, 2014 at 9:54 AM, Eric Seidel <eric at seidel.io> wrote:
> Would it easier to send the diff to Phab? I don't think the git history
> will be particularly illuminating.
>
> On Mon, Nov 17, 2014, at 07:45, Austin Seipp wrote:
>> 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/
>



-- 
Regards,

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

More information about the ghc-devs mailing list