Typechecker plugins: request for review and another workflow question

Fri Nov 14 17:45:48 UTC 2014

For what it's worth, I'd be very excited to have that feature in 7.10.

Iavor, is there anywhere I can read on how to try your solver for
type-level naturals?

Francesco

On 14 November 2014 18: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/
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs