Stream: wg-traits

Topic: design meeting 2019.12.02


nikomatsakis (Dec 02 2019 at 19:01, on Zulip):

Hey @WG-traits -- I probably should have written earlier -- but having just come back from vacation I'm rather discombobulated and not really in a place to have a meeting today. But maybe people can post updates here of interesting things instead, as a lightweight alternative

nikomatsakis (Dec 02 2019 at 19:02, on Zulip):
nikomatsakis (Dec 02 2019 at 19:02, on Zulip):
nikomatsakis (Dec 02 2019 at 19:03, on Zulip):
Jack Huey (Dec 02 2019 at 19:18, on Zulip):

A few of those PRs are from me

Jack Huey (Dec 02 2019 at 19:19, on Zulip):

A few smaller ones (like adding a regression test)

Jack Huey (Dec 02 2019 at 19:19, on Zulip):

But also a few bigger ones

Jack Huey (Dec 02 2019 at 19:19, on Zulip):

All the big one's I think you've seen

Jack Huey (Dec 02 2019 at 19:20, on Zulip):

Definitely I think look at https://github.com/rust-lang/chalk/pull/294, since rust-analyzer is currently using my branch

Jack Huey (Dec 02 2019 at 19:21, on Zulip):

But we can talk about PRs elsewhere

Jack Huey (Dec 02 2019 at 19:21, on Zulip):

But, I have also been thinking about https://github.com/rust-lang/chalk/issues/234

Jack Huey (Dec 02 2019 at 19:21, on Zulip):

And have been playing around with it locally

Jack Huey (Dec 02 2019 at 19:21, on Zulip):

(so this is more of a design topic)

Jack Huey (Dec 02 2019 at 19:22, on Zulip):

And probably worth a Hackmd doc

Jack Huey (Dec 02 2019 at 19:22, on Zulip):

But just generally, I more or less started thinking from your comments on that issue

Jack Huey (Dec 02 2019 at 19:23, on Zulip):

But I think the "proper" solution will end up being actually a mix of what you suggest

Jack Huey (Dec 02 2019 at 19:23, on Zulip):

So, for brevity, I'll just pose a few questions/thoughts:

nikomatsakis (Dec 02 2019 at 19:26, on Zulip):

@Jack Huey I was thinking about the "no recursion" change -- one thing that I think is suspicious in the PR (but also in master) is that it is definitely possible to wind up with an answer that "refines" a previous answer -- i.e., where a previous answer was ambig, the new answer might not be.

nikomatsakis (Dec 02 2019 at 19:26, on Zulip):

It's also possible to have the same answer appear multiple times with different region constraints.

nikomatsakis (Dec 02 2019 at 19:26, on Zulip):

I was thinking that the current handling for this is probably not very good

nikomatsakis (Dec 02 2019 at 19:26, on Zulip):

I believe your PR simply panics in this situation?

nikomatsakis (Dec 02 2019 at 19:26, on Zulip):

And that therefore we have no tests that exercise these paths?

detrumi (Dec 02 2019 at 19:29, on Zulip):

Chalk needs more tests in general (though rust-analyzer is doing a good job at uncovering bugs atm)

Jack Huey (Dec 02 2019 at 19:29, on Zulip):
  1. Why do we need a separate ProjectionEq and Normalize?
  2. Do we really need a separate idea for Projection and Placeholder type?
  3. Going off that, when we think about projections, I think you're right that we should also sort of associate a normalized value (or an inference variable) to it
  4. When we generate an answer to a ProjectionEq, that answer should I think take the form of Projection *as* Ty. This is important because if there are two *known* answers like <S as Trait1>::Item = u32 and <T as Trait1>::Item == i32, if we don't keep the information of the projection around for aggregation, then this could give an ambiguous answer, rather than <?0 as Trait1>::Item`
detrumi (Dec 02 2019 at 19:30, on Zulip):

Especially ra's analysis-stats, which finds bugs like #301

Jack Huey (Dec 02 2019 at 19:31, on Zulip):

@nikomatsakis um, yes my branch would panic. But so would master.

Jack Huey (Dec 02 2019 at 19:32, on Zulip):

Just mine panics when the answer would have been inserted, master will panic later (I'll have to hunt down the code, but it essentially assumes that the index increases by one when that method returns true, indicating an answer was inserted)

Jack Huey (Dec 02 2019 at 19:33, on Zulip):

There are no tests that exercise this path

Jack Huey (Dec 02 2019 at 19:37, on Zulip):

As far as tests, I'm not sure really the best approach with that. Because, it's not like there's an obvious area where we lack tests, it's just more that the tests that are there don't cover the cases they test fully. So, probably the best approach is to, as bug reports happens, really think about other similar tests that could be added too.

nikomatsakis (Dec 02 2019 at 19:39, on Zulip):

@Jack Huey yeah I think the thing to do is to file a follow-up issue, I might try to craft some tests that show the error path-way.

nikomatsakis (Dec 02 2019 at 19:40, on Zulip):

As for the way to handle normalization, that is indeed a complex topic, I've written some notes on it. I don't know what I think the best way to handle it is but it should be impossible to get <S as Foo>::Item to normalize to two distinct types (that is a language bug, if that is possible)

nikomatsakis (Dec 02 2019 at 19:41, on Zulip):

At the moment the disaggregator obviously doesn't handle such cases optimally, there's a bug filed on it, I was thinking that the best way might be for it to check -- if it sees a projection type and a normal type, it could cerainly do a query to see if the former normalizes to the latter -- but I'm not crazy about this answer.

nikomatsakis (Dec 02 2019 at 19:41, on Zulip):

Did you see my comment on the topic? I can go try to find it

nikomatsakis (Dec 02 2019 at 19:42, on Zulip):

That might be a good "design meeting" topic, or just an ad-hoc meeting -- to talk ove the current strategy and kind of explain it and explore some of the alternatives I see

Jack Huey (Dec 02 2019 at 19:52, on Zulip):

@nikomatsakis I can file a followup issue for the error path

Jack Huey (Dec 02 2019 at 19:52, on Zulip):

And yes, the comments were in the issue that I linked

Jack Huey (Dec 02 2019 at 19:52, on Zulip):

starting here: https://github.com/rust-lang/chalk/issues/234#issuecomment-528109851

Jack Huey (Dec 02 2019 at 19:54, on Zulip):

And yes, the projection shouldn't normalize to two distinct types, but there may be multiple answers like <S as Foo>... and <T as Foo>...

Jack Huey (Dec 02 2019 at 19:59, on Zulip):

And I think rather than having the ProjectionEq goal generate two separate clauses (Normalize... and the placeholder type), it just generates one <?0 as Foo>::Item is ?1 (where here I'm using "is" to say <?0 as Foo>::Item normalizes to ?1). Then the answers would be like <S as Foo>::Item is u32 and <T as Foo>::Item is i32. Or if we don't know what ?1 could be, we can also end up with <!1_0 as Foo>::Item is ?0 and this is equivalent to the placeholder type used today

Jack Huey (Dec 02 2019 at 20:00, on Zulip):

Of course, it seems a bit convoluted with the example, since there aren't other parameters, but you could imagine that this pattern follows

Jack Huey (Dec 02 2019 at 20:01, on Zulip):

Like I said, I've played around a bit and got it so it "works", but it's not 100% correct and not all tests are passing. But the idea is good I think

detrumi (Dec 02 2019 at 20:01, on Zulip):

As for a update from me: I started with a QuantifiedTy/QuantifiedApply refactor, and I'm looking at that panic that RA uncovered. For both, I'm running into the common theme that I don't understand what the code is (or should be) doing, so I'm putting some time in debugging stuff (with println's mostly, not a debugger), and I guess I should get into the habit of running examples through Chalki as well.

Jack Huey (Dec 02 2019 at 20:02, on Zulip):

CHALK_DEBUG=2 (or 1) is fantastic

detrumi (Dec 02 2019 at 20:03, on Zulip):

Ah, that's helpful (and should really be documented somewhere). Is 2 just more verbose?

Jack Huey (Dec 02 2019 at 20:04, on Zulip):

Yeah, 2 is much more verbose

Jack Huey (Dec 02 2019 at 20:05, on Zulip):

yeah, it's not really documented, but the debug!(...) statements are 2 and info!(...) is 1

detrumi (Dec 02 2019 at 20:09, on Zulip):

Heh, yeah that's quite some output

nikomatsakis (Dec 02 2019 at 20:21, on Zulip):

one thing I was considering was trying to port chalk's debug output to use the tracing module, which @David Barsky has been telling me is very cool

nikomatsakis (Dec 02 2019 at 20:21, on Zulip):

@Jack Huey and I were talking the other day about how to improve chalk's docs

nikomatsakis (Dec 02 2019 at 20:21, on Zulip):

seems like we need to include CHALK_DEBUG for sure.

Jack Huey (Dec 02 2019 at 20:24, on Zulip):

I left a comment on the issue mentioning chalk book we remember later

Jack Huey (Dec 02 2019 at 20:26, on Zulip):

That is one slight "regression" in the non-recursive branch is you no longer get the nested debug statements. But you gain a bit finer tracing. That just would require touching the chalk_macros crate to enable storing the Indent struct on the stack

Jack Huey (Dec 02 2019 at 20:26, on Zulip):

not difficult, but not something I wanted to touch

detrumi (Dec 02 2019 at 20:28, on Zulip):

seems like we need to include CHALK_DEBUG for sure.

Yeah, I'll get a PR up to make CONTRIBUTING.md slightly less outdated :slight_smile:

Jack Huey (Dec 02 2019 at 20:29, on Zulip):

Also, nudge https://github.com/rust-lang/chalk/issues/299

detrumi (Dec 02 2019 at 20:31, on Zulip):

Or set up tracing so you can exclude those added clauses, if that's possible

detrumi (Dec 02 2019 at 20:33, on Zulip):

It would be very cool if you could selectively get logging output from certain kinds of rules, while still running chalk like normal

Jack Huey (Dec 02 2019 at 20:34, on Zulip):

The only problem is then how do you exclude subgoals

Jack Huey (Dec 02 2019 at 20:35, on Zulip):

I guess you would have to "switch off" logging at a given stack depth

David Barsky (Dec 03 2019 at 02:59, on Zulip):

Bit of a late response, but: tracing is best used if you annotate all the units of work in an application/library (using a span: https://tracing.rs/tracing/span/index.html; syntax sugar also available: https://tracing.rs/tracing_attributes/attr.instrument.html). once you do, any data that's recorded can be filtered on, queried over, or switched on/off.

David Barsky (Dec 03 2019 at 02:59, on Zulip):

So to answer:

It would be very cool if you could selectively get logging output from certain kinds of rules, while still running chalk like normal

...tracing would let you do that, if you annotate those rules in a way that tracing can understand (whether that be via a string, module, or whatever)

David Barsky (Dec 03 2019 at 03:01, on Zulip):

Eliza had a neat blog post that demonstrated this in the context of a service: https://tokio.rs/blog/2019-08-tracing

Last update: Dec 12 2019 at 00:55UTC