Stream: wg-traits

Topic: design meeting 2020.01.13


Jack Huey (Jan 13 2020 at 18:54, on Zulip):

Hi @WG-traits

Jack Huey (Jan 13 2020 at 18:54, on Zulip):

Bit early

Jack Huey (Jan 13 2020 at 18:54, on Zulip):

But, let's figure out what we want to talk about today?

nikomatsakis (Jan 13 2020 at 18:55, on Zulip):

I was just pondering that

Jack Huey (Jan 13 2020 at 18:55, on Zulip):

So, one thing I was thinking about

Jack Huey (Jan 13 2020 at 18:55, on Zulip):

Was impl Trait

Jack Huey (Jan 13 2020 at 18:55, on Zulip):

So, we removed Opaque

Jack Huey (Jan 13 2020 at 18:55, on Zulip):

In favor of Alias

Jack Huey (Jan 13 2020 at 18:56, on Zulip):

But, a bit confused with this

Jack Huey (Jan 13 2020 at 18:57, on Zulip):

We could also discuss how we might want to handle yielding in the middle of solving

nikomatsakis (Jan 13 2020 at 18:57, on Zulip):

I've been thinking about the strategy for migrating and developing chalk. I've been thining in particular that it makes sense to be doing two things:

I was curious to discuss the first bullet point a bit in particular.

The second I think can be useful in part to help in validating chalk's role as a definitive semantics for Rust's trait system, as much as anything else.

Jack Huey (Jan 13 2020 at 18:57, on Zulip):

(does the design of my PR make sense, or do we want to do something else, basically)

nikomatsakis (Jan 13 2020 at 18:57, on Zulip):

But, a bit confused with this

we could discuss it, sure

Jack Huey (Jan 13 2020 at 18:57, on Zulip):

I've also been starting to write up some chalk goals: https://hackmd.io/VeMmXIYBRu2KdYbJDIpcFA?both

Jack Huey (Jan 13 2020 at 18:57, on Zulip):

kind of rough write now

nikomatsakis (Jan 13 2020 at 18:57, on Zulip):

We could also discuss how we might want to handle yielding in the middle of solving

ok, I didn't get a chance to look too closely at your PR yet but we could talk it over

Jack Huey (Jan 13 2020 at 18:57, on Zulip):

but mostly breaking them down into categories

Jack Huey (Jan 13 2020 at 18:58, on Zulip):

This is interesting to me, but I wouldn't be able to say much

nikomatsakis (Jan 13 2020 at 18:59, on Zulip):

I spent some time filling out https://github.com/rust-lang/wg-traits/projects earlier --

nikomatsakis (Jan 13 2020 at 18:59, on Zulip):

(nothing since last week)

Jack Huey (Jan 13 2020 at 19:00, on Zulip):

Do we want to use that "chalk development" project there? Or make one in rust-lang/chalk

nikomatsakis (Jan 13 2020 at 19:00, on Zulip):

but one thing I was thinking of doing today is trying to fill out a few more such goals and brain dump in steps along the way

nikomatsakis (Jan 13 2020 at 19:00, on Zulip):

Do we want to use that "chalk development" project there? Or make one in rust-lang/chalk

a good question

nikomatsakis (Jan 13 2020 at 19:00, on Zulip):

I guess it depends how much "interaction" we expect perhaps

detrumi (Jan 13 2020 at 19:01, on Zulip):

interaction with rustc you mean?

nikomatsakis (Jan 13 2020 at 19:01, on Zulip):

one of the questions this group has wrestled with a lot is figuring out its scope

Jack Huey (Jan 13 2020 at 19:01, on Zulip):

I personally feel like, unless there are cross-project concerns, it would be best in rust-lang/chalk

nikomatsakis (Jan 13 2020 at 19:01, on Zulip):

(well I meant like "is the focus just on chalk" or does it encompass rustc, and how much would we expect people to go back and forth between them)

nikomatsakis (Jan 13 2020 at 19:02, on Zulip):

I guess I don't care too much which place we put things

nikomatsakis (Jan 13 2020 at 19:02, on Zulip):

(I wonder how easy it is to move)

Jack Huey (Jan 13 2020 at 19:02, on Zulip):

hmm, can you even move projects? not sure

nikomatsakis (Jan 13 2020 at 19:03, on Zulip):

I think you cannot

nikomatsakis (Jan 13 2020 at 19:03, on Zulip):

at least I don't see an obvious way

nikomatsakis (Jan 13 2020 at 19:03, on Zulip):

I personally feel like, unless there are cross-project concerns, it would be best in rust-lang/chalk

I agree this is where I would naively expect things to be

Jack Huey (Jan 13 2020 at 19:03, on Zulip):

anyways, it's 2:03, maybe we should start with a sync-up?

nikomatsakis (Jan 13 2020 at 19:03, on Zulip):

yes

nikomatsakis (Jan 13 2020 at 19:04, on Zulip):

well, for me, last week somehow got very full, and I spent most of my "trait related" time pondering #57893, a soundness bug

nikomatsakis (Jan 13 2020 at 19:04, on Zulip):

I think the work on that plausibly falls under this group, if we take the more expansive definition :)

Jack Huey (Jan 13 2020 at 19:04, on Zulip):

I haven't looked at that in a while

Jack Huey (Jan 13 2020 at 19:04, on Zulip):

but I remember it

Jack Huey (Jan 13 2020 at 19:05, on Zulip):

As for me, I made a PR to refactor the test infra a bit

nikomatsakis (Jan 13 2020 at 19:05, on Zulip):

I did some reviewing or PRs and I am contemplating in particular https://github.com/rust-lang/rust/pull/67717 and optimization of canonicalization, which I need to follow up with @Ben Lewis about (probably)

Jack Huey (Jan 13 2020 at 19:05, on Zulip):

(https://github.com/rust-lang/chalk/pull/317)

Jack Huey (Jan 13 2020 at 19:05, on Zulip):

Also, been looking at some of the rust-analyzer reported issues

Jack Huey (Jan 13 2020 at 19:06, on Zulip):

I have different different branches for rust-lang/chalk#301

detrumi (Jan 13 2020 at 19:06, on Zulip):

And I started with the renaming to Alias, though in some places it wasn't really clear whether other kinds of aliases weren't implemented yet or whether they will be handled like associated types

Jack Huey (Jan 13 2020 at 19:06, on Zulip):

@detrumi glad you're here. definitely I think we should discuss this

nikomatsakis (Jan 13 2020 at 19:07, on Zulip):

yeah, I was going to say the same thing

Jack Huey (Jan 13 2020 at 19:07, on Zulip):

Let's start with that?

nikomatsakis (Jan 13 2020 at 19:07, on Zulip):

Sounds good

detrumi (Jan 13 2020 at 19:07, on Zulip):

Sure

Jack Huey (Jan 13 2020 at 19:07, on Zulip):

If we have time later, we can get into the rust-analyzer issues

Jack Huey (Jan 13 2020 at 19:08, on Zulip):

But anyways, I was looking into how to maybe reimplement impl Trait

nikomatsakis (Jan 13 2020 at 19:08, on Zulip):

So, in terms of aliases, rust has 3 notion of aliases. Each is handled somewhat differently in rustc but have a lot of similarities

Jack Huey (Jan 13 2020 at 19:08, on Zulip):

And I think maybe I'm not understanding what we expect Alias to be correctly

detrumi (Jan 13 2020 at 19:08, on Zulip):

Right, like commented here: https://github.com/rust-lang/chalk/pull/320/files#diff-9cded8099833735b25a53f395aa7f9f3R262

Jack Huey (Jan 13 2020 at 19:09, on Zulip):

yes

Jack Huey (Jan 13 2020 at 19:09, on Zulip):

though, impl Trait doesn't really seem to fit the others

nikomatsakis (Jan 13 2020 at 19:09, on Zulip):

well so

Jack Huey (Jan 13 2020 at 19:10, on Zulip):

Namely, the associated type and type XXX = ... essentially points to another type

nikomatsakis (Jan 13 2020 at 19:10, on Zulip):

it really does :)

detrumi (Jan 13 2020 at 19:10, on Zulip):

Isn't that <T as Trait>::...? (just a guess)

Jack Huey (Jan 13 2020 at 19:10, on Zulip):

(a type function, you said another time)

nikomatsakis (Jan 13 2020 at 19:10, on Zulip):

or at least I think it does

nikomatsakis (Jan 13 2020 at 19:10, on Zulip):

so, here is why

Jack Huey (Jan 13 2020 at 19:10, on Zulip):

@nikomatsakis maybe want to elaborate and I'll wait a bit

nikomatsakis (Jan 13 2020 at 19:10, on Zulip):

to start, I'm talking here about the "opaque" view of an impl Trait

nikomatsakis (Jan 13 2020 at 19:10, on Zulip):

that is, I'm not talking about the logic to figure out what the hidden type is

nikomatsakis (Jan 13 2020 at 19:11, on Zulip):

but more about what happens when you use a fn foo() -> impl trait (or whatever) "from the outside"

nikomatsakis (Jan 13 2020 at 19:11, on Zulip):

in that case, we are really always dealing with a placeholder type

nikomatsakis (Jan 13 2020 at 19:11, on Zulip):

where the only things we know are (a) the declared trait bounds and (b) we also have to think about auto-trait leakage :)

nikomatsakis (Jan 13 2020 at 19:12, on Zulip):

let's assume for a moment we know the hidden type

nikomatsakis (Jan 13 2020 at 19:12, on Zulip):

sorry, let's assume we are rustc, and we know the hidden type

nikomatsakis (Jan 13 2020 at 19:12, on Zulip):

we want to generate rules for chalk to use for proving bounds and things

nikomatsakis (Jan 13 2020 at 19:13, on Zulip):

so given say a type Foo = impl A + B+ C; // hidden type T0

nikomatsakis (Jan 13 2020 at 19:13, on Zulip):

and given some kind of chalk type representing an "alias placeholder", let's call it !Foo

nikomatsakis (Jan 13 2020 at 19:13, on Zulip):

then we might make rules like

nikomatsakis (Jan 13 2020 at 19:14, on Zulip):
Implemented(!Foo: A)
Implemented(!Foo: B)
Implemented(!Foo: C)
Implemented(!Foo: Send) :- Implemented(T0 : Send)
nikomatsakis (Jan 13 2020 at 19:14, on Zulip):

the more general case would be something like:

Implemented(!Foo: Trait)

Jack Huey (Jan 13 2020 at 19:16, on Zulip):

this makes sense

Jack Huey (Jan 13 2020 at 19:17, on Zulip):

but not necessarily how it fits Alias (or how that's the "same" as an associated type)

nikomatsakis (Jan 13 2020 at 19:17, on Zulip):

the three sorts of aliases I see are:

nikomatsakis (Jan 13 2020 at 19:18, on Zulip):

I see the three as behaving very similarly in that:

but the rules we use to satisfy this goal will depend on the kind of alias

nikomatsakis (Jan 13 2020 at 19:19, on Zulip):
nikomatsakis (Jan 13 2020 at 19:19, on Zulip):

that said, I remember that initially I was hoping to have only one alias type, and to know from context if it was a placeholder or not (as rustc does)

nikomatsakis (Jan 13 2020 at 19:19, on Zulip):

however, I convinced myself that was not viable, and we would need distinct placeholder types

nikomatsakis (Jan 13 2020 at 19:20, on Zulip):

but not necessarily how it fits Alias (or how that's the "same" as an associated type)

I guess I would say that it doesn't necessarily have to be grouped together -- we could make more cases -- but the way we had implemented it, where the bounds were part of the type, was not correct

nikomatsakis (Jan 13 2020 at 19:20, on Zulip):

i.e., it's not like dyn

nikomatsakis (Jan 13 2020 at 19:20, on Zulip):

impl trait values have to have a def-id they are based off of

nikomatsakis (Jan 13 2020 at 19:20, on Zulip):

so that we can generate the "auto trait" rules etc

nikomatsakis (Jan 13 2020 at 19:21, on Zulip):

and because with type Foo = impl Trait; type Bar = impl Trait;, Foo and Bar are not the same type

detrumi (Jan 13 2020 at 19:22, on Zulip):

Not sure I understand; would that mean AliasTy would become an enum to hold that def-id?

nikomatsakis (Jan 13 2020 at 19:22, on Zulip):

On a related note, one of the things I've been thinking about with the type transition is that we should try to move rustc and chalk closer together by refactoring them both. so e.g. chalk has far fewer categories, and I think we might experiment with merging some of rustc's categories to make them line up. This may be a pain because parts of rustc wish to distinguish between types that chalk wouldn't, and we can decide if it's worth it -- it will also have some memory usage implications, which we would want to measure. In other words, I doubt we can pick the perfect variants a priori

nikomatsakis (Jan 13 2020 at 19:22, on Zulip):

Not sure I understand; would that mean AliasTy would become an enum to hold that def-id?

well, there are two choices

nikomatsakis (Jan 13 2020 at 19:23, on Zulip):

first, it already has a def-id

nikomatsakis (Jan 13 2020 at 19:23, on Zulip):

well, it has an AssociatedTyId or something

nikomatsakis (Jan 13 2020 at 19:23, on Zulip):

which in rustc would just be a def-id anyway

detrumi (Jan 13 2020 at 19:23, on Zulip):

Ah right, AssocTypeId is just a DefId

nikomatsakis (Jan 13 2020 at 19:23, on Zulip):

we can either say that, from Chalk's POV, there is just AliasDefId

Jack Huey (Jan 13 2020 at 19:23, on Zulip):

Isn't the point of the Ty vs TyData split to (somewhat) allow differences in types

nikomatsakis (Jan 13 2020 at 19:23, on Zulip):

and then have the chalk-solve have some callbacks to ask the RustIrDatabase what sort of alias it is

Jack Huey (Jan 13 2020 at 19:23, on Zulip):

or is that solely for interning

nikomatsakis (Jan 13 2020 at 19:24, on Zulip):

Isn't the point of the Ty vs TyData split to (somewhat) allow differences in types

this was meant to be temporary, in my mind

nikomatsakis (Jan 13 2020 at 19:24, on Zulip):

until we had converged on a single definition

nikomatsakis (Jan 13 2020 at 19:24, on Zulip):

we still need the split mind you

nikomatsakis (Jan 13 2020 at 19:24, on Zulip):

to permit interning vs not interning

nikomatsakis (Jan 13 2020 at 19:24, on Zulip):

but I did want to converge eventually on rustc sharing the same enum as rust-analyzer

nikomatsakis (Jan 13 2020 at 19:25, on Zulip):

well, ideally, rustc and rust-analyzer sharing bigger libraries (like chalk) that are based around this enum

detrumi (Jan 13 2020 at 19:25, on Zulip):

The enum would live in the type library, right?

nikomatsakis (Jan 13 2020 at 19:25, on Zulip):

right

nikomatsakis (Jan 13 2020 at 19:25, on Zulip):

the thing that I meant to be temporary, specifically:

nikomatsakis (Jan 13 2020 at 19:25, on Zulip):

I imagined that in rustc integration, when you invoke data() we would generate lazilly a chalk enum representation

nikomatsakis (Jan 13 2020 at 19:26, on Zulip):

(or maybe eagerly, if you have -Zchalk)

nikomatsakis (Jan 13 2020 at 19:26, on Zulip):

but the rest of rustc goes on using its current types for now

nikomatsakis (Jan 13 2020 at 19:26, on Zulip):

but I don't think we want that long term

nikomatsakis (Jan 13 2020 at 19:26, on Zulip):

for one thing, it's a waste of memory

nikomatsakis (Jan 13 2020 at 19:26, on Zulip):

but it seems convenient in order to get chalk-solve integrated

nikomatsakis (Jan 13 2020 at 19:27, on Zulip):

(make sense?)

Jack Huey (Jan 13 2020 at 19:27, on Zulip):

I think that makes sense

Jack Huey (Jan 13 2020 at 19:27, on Zulip):

I'll have to think about it more

detrumi (Jan 13 2020 at 19:27, on Zulip):

Wouldn't changing rustc's types take a lot of refactoring?

nikomatsakis (Jan 13 2020 at 19:27, on Zulip):

yes :)

nikomatsakis (Jan 13 2020 at 19:28, on Zulip):

the alternative would be to move chalk to be the same as rustc

nikomatsakis (Jan 13 2020 at 19:28, on Zulip):

I imagine we will do some of both

detrumi (Jan 13 2020 at 19:28, on Zulip):

Right, because translating between representations would be expensive in its own way

nikomatsakis (Jan 13 2020 at 19:28, on Zulip):

I'm a bit annoyed at this aspect of rust's design really

nikomatsakis (Jan 13 2020 at 19:28, on Zulip):

in particular, it seems annoying that how you group your enum variants has real impact on performance and memory usage

nikomatsakis (Jan 13 2020 at 19:29, on Zulip):

rustc takes a "maximal" view and makes a ton of variants

nikomatsakis (Jan 13 2020 at 19:29, on Zulip):

but then you commonly have match statements grouping lots of things together

nikomatsakis (Jan 13 2020 at 19:29, on Zulip):

chalk uses nested variants, which is nice, but then if you need to do recursive matching

nikomatsakis (Jan 13 2020 at 19:29, on Zulip):

that's going to be a bit less optimal code

nikomatsakis (Jan 13 2020 at 19:29, on Zulip):

and we're going to use more memory in the memory layout

nikomatsakis (Jan 13 2020 at 19:29, on Zulip):

there's some kind of missing feature here but oh well :)

nikomatsakis (Jan 13 2020 at 19:30, on Zulip):

(we've sort of known this for a while, but it's hard to fix)

nikomatsakis (Jan 13 2020 at 19:30, on Zulip):

anyway to circle back to alias's for a second --

nikomatsakis (Jan 13 2020 at 19:30, on Zulip):

if we just had AliasDefId

nikomatsakis (Jan 13 2020 at 19:30, on Zulip):

then presumably we could have a method like alias_kind in RustIrDatabase that tells chalk-solve what sort of alias it is

nikomatsakis (Jan 13 2020 at 19:31, on Zulip):

and hence which kind of AliasEq and other rules to generate for it

nikomatsakis (Jan 13 2020 at 19:31, on Zulip):

though this again is a very ... "chalk-centric" POV

nikomatsakis (Jan 13 2020 at 19:32, on Zulip):

i.e., maybe parts of rustc might want to distinguish them and it would be annoying that they had only one variant and had to use helper methods to figure out what sort of alias they have

detrumi (Jan 13 2020 at 19:32, on Zulip):

Won't that be the case in Chalk as well?

nikomatsakis (Jan 13 2020 at 19:33, on Zulip):

yeah, in chalk-solve, just not in unify etc

detrumi (Jan 13 2020 at 19:33, on Zulip):

hmm

nikomatsakis (Jan 13 2020 at 19:33, on Zulip):

so maybe we want 3 variants ...

nikomatsakis (Jan 13 2020 at 19:33, on Zulip):

... that unify treats the same ...

Jack Huey (Jan 13 2020 at 19:34, on Zulip):

:shrug:‍♂️

Jack Huey (Jan 13 2020 at 19:34, on Zulip):

@detrumi did you want to try to implement this?

nikomatsakis (Jan 13 2020 at 19:35, on Zulip):

Wouldn't changing rustc's types take a lot of refactoring?

I guess this might argue for matching rustc's design

detrumi (Jan 13 2020 at 19:35, on Zulip):

I'd like to try, at least :slight_smile:

nikomatsakis (Jan 13 2020 at 19:35, on Zulip):

after all, refactoring chalk is easier thus far ;)

nikomatsakis (Jan 13 2020 at 19:35, on Zulip):

though I do appreciate a "smaller" type enum that tries to highlight the essential behavior of each type

nikomatsakis (Jan 13 2020 at 19:35, on Zulip):

but I also think that trying to group these 3 sorts of "aliases" together only kind of works

Jack Huey (Jan 13 2020 at 19:36, on Zulip):

If possible (and elegant), I would also prefer a smaller type enum

nikomatsakis (Jan 13 2020 at 19:36, on Zulip):

I see them as kind of points along a spectrum, but they are distinct points (and you have to squint a bit, thanks to stuff like auto trait leakage)

Jack Huey (Jan 13 2020 at 19:38, on Zulip):

Ok if @detrumi wants to try to implement this, then I'll do other stuff :)

Jack Huey (Jan 13 2020 at 19:38, on Zulip):

But I think it would be better to "fix" impl Trait sooner rather than later

Jack Huey (Jan 13 2020 at 19:38, on Zulip):

since rust-analyzer will probably want the fixes for other issues

nikomatsakis (Jan 13 2020 at 19:38, on Zulip):

yes, I think it's good to be presenting a coherent view of the type enum

detrumi (Jan 13 2020 at 19:39, on Zulip):

I'll need a bit more detail to get started, but it seems doable

Jack Huey (Jan 13 2020 at 19:39, on Zulip):

since rust-analyzer will probably want the fixes for other issues

see https://rust-lang.zulipchat.com/#narrow/stream/144729-wg-traits/topic/ambiguous.20answer.20replacement/near/185302669

Jack Huey (Jan 13 2020 at 19:39, on Zulip):

Anything else for impl Trait or Alias right now?

nikomatsakis (Jan 13 2020 at 19:40, on Zulip):

I think that covers this

nikomatsakis (Jan 13 2020 at 19:40, on Zulip):

since rust-analyzer will probably want the fixes for other issues

yeah, I see, sorry @Florian Diebold ...

Jack Huey (Jan 13 2020 at 19:41, on Zulip):

Speaking of rust-analyzer bugs

Jack Huey (Jan 13 2020 at 19:41, on Zulip):

I've looked at two

nikomatsakis (Jan 13 2020 at 19:41, on Zulip):

yep

detrumi (Jan 13 2020 at 19:41, on Zulip):

nice segway :smirk:

Jack Huey (Jan 13 2020 at 19:41, on Zulip):

this one: https://github.com/rust-lang/chalk/issues/302

Jack Huey (Jan 13 2020 at 19:41, on Zulip):

So, we kind of saw this coming

Jack Huey (Jan 13 2020 at 19:42, on Zulip):

And this one: https://github.com/rust-lang/chalk/issues/301

Jack Huey (Jan 13 2020 at 19:42, on Zulip):

(and then I also found a potential bug: https://github.com/rust-lang/chalk/issues/318)

Jack Huey (Jan 13 2020 at 19:42, on Zulip):

all of these directly come from truncation

Jack Huey (Jan 13 2020 at 19:43, on Zulip):

those the first (302) actually is a slightly larger issue around ambiguity (but in this case is from truncation)

Jack Huey (Jan 13 2020 at 19:43, on Zulip):

but @nikomatsakis was suggesting that maybe we don't do truncation at all

Jack Huey (Jan 13 2020 at 19:44, on Zulip):

That would be fairly easy to test, I think

nikomatsakis (Jan 13 2020 at 19:44, on Zulip):

to be specific, I think we would turn truncation into something like a boolean test

nikomatsakis (Jan 13 2020 at 19:44, on Zulip):

if it exceeds the threshold, we would flounder

nikomatsakis (Jan 13 2020 at 19:45, on Zulip):

rustc has a similar rule where it just plain forbids the creation of types larger than a certain size

Jack Huey (Jan 13 2020 at 19:45, on Zulip):

there are really only two places we truncate right now: in get_or_create_table_for_subgoal

Jack Huey (Jan 13 2020 at 19:45, on Zulip):

and in: truncate_returned

nikomatsakis (Jan 13 2020 at 19:45, on Zulip):

yeah

Jack Huey (Jan 13 2020 at 19:45, on Zulip):

for the first, it's pretty easy: we just Flounder the table

Jack Huey (Jan 13 2020 at 19:46, on Zulip):

for the second, we could just...not?

nikomatsakis (Jan 13 2020 at 19:46, on Zulip):

/me ponders

nikomatsakis (Jan 13 2020 at 19:46, on Zulip):

what rustc actually does is to abort I think

nikomatsakis (Jan 13 2020 at 19:46, on Zulip):

like, hard abort compilation

nikomatsakis (Jan 13 2020 at 19:46, on Zulip):

I'd rather not go that far if we can avoid it

Jack Huey (Jan 13 2020 at 19:46, on Zulip):

I don't think we want that

nikomatsakis (Jan 13 2020 at 19:47, on Zulip):

(but we may wish to propagate back some kind of error)

nikomatsakis (Jan 13 2020 at 19:47, on Zulip):

in any case the reason we apply that in both places is to prevent infinite loops

Jack Huey (Jan 13 2020 at 19:47, on Zulip):

if anything, we could do as we do with NegativeCycle and propogate out immediately

nikomatsakis (Jan 13 2020 at 19:47, on Zulip):

right

nikomatsakis (Jan 13 2020 at 19:47, on Zulip):

and that may be reasonable

nikomatsakis (Jan 13 2020 at 19:47, on Zulip):

in any case the reason we apply that in both places is to prevent infinite loops

I'm trying to think about the case of "if you just apply it when creating new tables"... whta can go wrong...

nikomatsakis (Jan 13 2020 at 19:48, on Zulip):

I suspect there can be some kind of cycle but not entirely sure how to build it

Jack Huey (Jan 13 2020 at 19:48, on Zulip):

This also hits on the idea of performance too

nikomatsakis (Jan 13 2020 at 19:48, on Zulip):

regardless, I think the other question is:

nikomatsakis (Jan 13 2020 at 19:48, on Zulip):

when you lift the limit in rust-analyzer

nikomatsakis (Jan 13 2020 at 19:48, on Zulip):

I believe it starts to have other problems

Jack Huey (Jan 13 2020 at 19:48, on Zulip):

yes, let me see if I can find that

nikomatsakis (Jan 13 2020 at 19:48, on Zulip):

and it seems like we need to address those, rigit?

Jack Huey (Jan 13 2020 at 19:48, on Zulip):

we talked about that shortly

Jack Huey (Jan 13 2020 at 19:48, on Zulip):

https://rust-lang.zulipchat.com/#narrow/stream/185405-t-compiler.2Fwg-rls-2.2E0/topic/Changing.20CHALK_SOLVER_MAX_SIZE/near/184864153

detrumi (Jan 13 2020 at 19:49, on Zulip):

So, different/wrong answers

Jack Huey (Jan 13 2020 at 19:49, on Zulip):

no, I think just hanging

Jack Huey (Jan 13 2020 at 19:49, on Zulip):

I think as long as we have a way to prevent Chalk from hanging, we should be fine

Jack Huey (Jan 13 2020 at 19:51, on Zulip):

But this also opens a bit of a design problem:

Jack Huey (Jan 13 2020 at 19:51, on Zulip):

If we expect that at some point, there will be a large program

Jack Huey (Jan 13 2020 at 19:51, on Zulip):

(even if we are super fast)

Jack Huey (Jan 13 2020 at 19:51, on Zulip):

we will take a long time

Jack Huey (Jan 13 2020 at 19:51, on Zulip):

and we want the caller to say "that's enough, I don't care"

Jack Huey (Jan 13 2020 at 19:52, on Zulip):

but, what do we do:

Jack Huey (Jan 13 2020 at 19:52, on Zulip):

do we just say "I got nothing"

Jack Huey (Jan 13 2020 at 19:52, on Zulip):

or do we try to give some kind of hint

nikomatsakis (Jan 13 2020 at 19:52, on Zulip):

yeah this is the subject of your PR, right?

Jack Huey (Jan 13 2020 at 19:52, on Zulip):

Slightly

Jack Huey (Jan 13 2020 at 19:53, on Zulip):

so with my PR, I basically allow the solving to be cancelled at any point

Jack Huey (Jan 13 2020 at 19:53, on Zulip):

and it'll just give a suggestion with any answers that have already come through

Jack Huey (Jan 13 2020 at 19:53, on Zulip):

(even though the full aggregated answer isn't available)

Jack Huey (Jan 13 2020 at 19:54, on Zulip):

I talk a bit about this in the PR desc.

Jack Huey (Jan 13 2020 at 19:54, on Zulip):

but I could see us in the future allowing cancellation based on the current aggregated answer

Jack Huey (Jan 13 2020 at 19:54, on Zulip):

or to also extend the suggested answer by potential future answers

nikomatsakis (Jan 13 2020 at 19:55, on Zulip):

ok so

nikomatsakis (Jan 13 2020 at 19:55, on Zulip):

in this version you are threading down a "should continue" closure

Jack Huey (Jan 13 2020 at 19:55, on Zulip):

yeah

nikomatsakis (Jan 13 2020 at 19:55, on Zulip):

which gets invoked periodically

nikomatsakis (Jan 13 2020 at 19:55, on Zulip):

and which forces a QuantumExceeded result if it is true?

Jack Huey (Jan 13 2020 at 19:56, on Zulip):

it gets invoked anytime Chalk returns a QuantumExceeded

nikomatsakis (Jan 13 2020 at 19:56, on Zulip):

skimming the commits I somehow missed where should_continue() gets called

detrumi (Jan 13 2020 at 19:56, on Zulip):

I'd imagine that RA would want a partial answer, while rustc would only want the exact answer?

nikomatsakis (Jan 13 2020 at 19:56, on Zulip):

it gets invoked anytime Chalk returns a QuantumExceeded

oh, I see

Jack Huey (Jan 13 2020 at 19:56, on Zulip):

so, we're still at the mercy of the engine if no QuantumExceeded ever gets called

nikomatsakis (Jan 13 2020 at 19:56, on Zulip):

interesting

nikomatsakis (Jan 13 2020 at 19:56, on Zulip):

ok

nikomatsakis (Jan 13 2020 at 19:56, on Zulip):

not quite what I imagined at first

nikomatsakis (Jan 13 2020 at 19:56, on Zulip):

this is making me think btw

Jack Huey (Jan 13 2020 at 19:56, on Zulip):

but if QuantumExceeded never gets called, then we are on the happy path

nikomatsakis (Jan 13 2020 at 19:57, on Zulip):

that it'd be pretty nice to be documenting this high-level flow in the chalk book

Jack Huey (Jan 13 2020 at 19:57, on Zulip):

that it'd be pretty nice to be documenting this high-level flow in the chalk book

yes, I'm going to write chalk-engine documentation in the book at some point

nikomatsakis (Jan 13 2020 at 19:57, on Zulip):

it seems like it might be useful also

nikomatsakis (Jan 13 2020 at 19:58, on Zulip):

to be able to thread down said closure, perhaps as part of the Context or whatever

nikomatsakis (Jan 13 2020 at 19:58, on Zulip):

(but that's fine)

nikomatsakis (Jan 13 2020 at 19:58, on Zulip):

we can change exactly when/where/how it gets invoked

nikomatsakis (Jan 13 2020 at 19:58, on Zulip):

but the main thing is, if it is invoked, you get back kind of "what we got so far"

Jack Huey (Jan 13 2020 at 19:59, on Zulip):

another semi-related issue is: https://github.com/rust-lang/chalk/issues/260

Jack Huey (Jan 13 2020 at 19:59, on Zulip):

which relates to the idea of "cancellation"

Jack Huey (Jan 13 2020 at 20:00, on Zulip):

but the main thing is, if it is invoked, you get back kind of "what we got so far"

which I'm just doing a Guidance(Suggested(current_subst))

detrumi (Jan 13 2020 at 20:00, on Zulip):

should_continue is actually just cancellation from within instead of from outside

Jack Huey (Jan 13 2020 at 20:00, on Zulip):

should_continue is actually just cancellation from within instead of from outside

what do you mean?

Jack Huey (Jan 13 2020 at 20:00, on Zulip):

But, it's 3:00, so I'll give a quick summary of the meeting:

detrumi (Jan 13 2020 at 20:01, on Zulip):

cancellation and should_continue seem very similar, the only difference is who decides to stop the search (and for what reason)

nikomatsakis (Jan 13 2020 at 20:03, on Zulip):

but the main thing is, if it is invoked, you get back kind of "what we got so far"

which I'm just doing a Guidance(Suggested(current_subst))

interesting, yes. it seems like we should report that it's partial somehow

nikomatsakis (Jan 13 2020 at 20:03, on Zulip):

but I'm :+1: on the PR overall

nikomatsakis (Jan 13 2020 at 20:03, on Zulip):

But, it's 3:00, so I'll give a quick summary of the meeting:

:heart:

Jack Huey (Jan 13 2020 at 20:04, on Zulip):
Jack Huey (Jan 13 2020 at 20:04, on Zulip):

Did I miss anything?

Jack Huey (Jan 13 2020 at 20:04, on Zulip):
Jack Huey (Jan 13 2020 at 20:04, on Zulip):

that's very much an oversimplification

Jack Huey (Jan 13 2020 at 20:05, on Zulip):

Also, for any who didn't see: I'm working on writing down some chalk goals: https://hackmd.io/VeMmXIYBRu2KdYbJDIpcFA?both

Jack Huey (Jan 13 2020 at 20:05, on Zulip):

feel free to add anything you feel is important

Jack Huey (Jan 13 2020 at 20:06, on Zulip):

After I list them, I'll try to prioritize and add them to a github project (either on rust-lang/chalk or rust-lang/wg-traits)

detrumi (Jan 13 2020 at 20:09, on Zulip):

Maybe we should have one board for chalk changes, and one for rustc-chalk integration. Though it's not always clear what goes where then :slight_smile:

Jack Huey (Jan 13 2020 at 20:10, on Zulip):

I think that's the plan

Last update: Jun 07 2020 at 09:50UTC