Stream: wg-traits

Topic: an approximate solver for chalk?


nikomatsakis (Jan 06 2020 at 20:23, on Zulip):

One of the things that @pnkfelix and I were discussing -- basically, maybe it would make sense to build something more like rustc's engine, but operating on lowered chalk predicates? rustc's engine is quirky but of course it works "well enough" for rustc today, and it might make it easier to adopt chalk into rustc sooner rather than later.

Following up from that, I was pondering another possible design, one closer to the older 'recursive' solver that chalk used to have before the SLG solver. In short, it was always looking for a unique solution, unlike the existing chalk-engine solver that is based around finding exact solutions (and then having an outer layer that stops asking for more answers). I do remember we had some problems where the recursive solver wasn't strong enough to handle some cases, though I can't remember exactly what (@scalexm maybe remembers).

Anyway, I think that one of these two things might make sense as a way to get chalk integrated "sooner rather than later". But I think this is something to consider more as a second step, once we've integrated the chalk-solve crate into rustc.

matklad (Jan 06 2020 at 20:26, on Zulip):

build something more like rustc's engine, but operating on lowered chalk predicates?

Can we refactor existing solver from within such that it operates on the said input format?

matklad (Jan 06 2020 at 20:26, on Zulip):

(existing rustc solver that is)

matklad (Jan 06 2020 at 20:26, on Zulip):

This has a benefit of having only two parallel solvers, and not three, at any given point in time)

nikomatsakis (Jan 06 2020 at 20:33, on Zulip):

I wondered about that path

nikomatsakis (Jan 06 2020 at 20:33, on Zulip):

I think it's roughly equivalent

nikomatsakis (Jan 06 2020 at 20:33, on Zulip):

That is, I think the goal would be to build up the solver in chalk and then asap remove the one from rustc

nikomatsakis (Jan 06 2020 at 20:33, on Zulip):

Well I guess the question is can we do it gradually within rustc

nikomatsakis (Jan 06 2020 at 20:33, on Zulip):

I don't see how, but maybe

nikomatsakis (Jan 06 2020 at 20:34, on Zulip):

Really the most important thing here -- probably -- is to figure out the caching questions for 'lowering'

nikomatsakis (Jan 06 2020 at 20:34, on Zulip):

Also, a related question:

nikomatsakis (Jan 06 2020 at 20:34, on Zulip):

I've been describing a design that merges chalk types with rust types by having two parallel definitions that will eventually merge

nikomatsakis (Jan 06 2020 at 20:35, on Zulip):

But this could be a performance hazard, and I guess the goal should probably be to merge the type definitions sooner rather than later

nikomatsakis (Jan 06 2020 at 20:35, on Zulip):

Probably "just" rote work within rustc

nikomatsakis (Jan 06 2020 at 20:35, on Zulip):

(That could be done gradually, though)

nikomatsakis (Jan 06 2020 at 20:35, on Zulip):

i.e., we could gradually refactor rustc's enum until it basically matches the chalk enum

nikomatsakis (Jan 06 2020 at 20:36, on Zulip):

which would probably be good, since it might inform whether chalk's enum has the right set of variants (in particular, I think we might want to extract the integral / floating point types out, because of the way that rustc's integer literals work)

Last update: Jun 07 2020 at 10:35UTC