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 <a...@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.diatc...@gmail.com] >> *Sent:* 10 November 2014 19:15 >> *To:* Adam Gundry >> *Cc:* ghc-devs@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 <a...@well-typed.com >> <mailto:a...@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@haskell.org > http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
