Stream: wg-traits

Topic: coinduction unsoundness


Jack Huey (Oct 30 2019 at 20:54, on Zulip):

Well, in my quest to un-overengineer my fix, I managed to remove the recursion in pursue_strand (so no more pursue_strand_recursively)

Jack Huey (Oct 30 2019 at 20:54, on Zulip):

whoops?

nikomatsakis (Oct 30 2019 at 21:26, on Zulip):

huh

nikomatsakis (Oct 30 2019 at 21:26, on Zulip):

I don't really understand that :)

Jack Huey (Oct 30 2019 at 22:42, on Zulip):

(also, that "whoops?" was definitely sarcasm. Removing the recursion is great, I think)

Jack Huey (Oct 30 2019 at 22:42, on Zulip):

I'm cleaning up some last bits of things and then I'll make a PR :)

Jack Huey (Oct 30 2019 at 23:10, on Zulip):

@nikomatsakis https://github.com/rust-lang/chalk/pull/272

nikomatsakis (Oct 31 2019 at 18:08, on Zulip):

(also, that "whoops?" was definitely sarcasm. Removing the recursion is great, I think)

interesting. I'll take a look later!

Jack Huey (Nov 01 2019 at 16:06, on Zulip):

@nikomatsakis Was wondering if you have had time to peek at the PR? I'm actually curious if it will solve the infinite stack growth problem in rust-analyzer since it removes the recursion. If nothing else, it might help make it easier to debug?

nikomatsakis (Nov 01 2019 at 16:06, on Zulip):

I'm actually skimming it now

Jack Huey (Nov 01 2019 at 16:07, on Zulip):

Awesome

nikomatsakis (Nov 01 2019 at 16:10, on Zulip):

basically, you made us loop in pursue_strand, instead of having it recursively invoke itself?

nikomatsakis (Nov 01 2019 at 16:10, on Zulip):

I don't think this will help with that particular problem

Jack Huey (Nov 01 2019 at 16:13, on Zulip):

Yep, basically

nikomatsakis (Nov 01 2019 at 16:14, on Zulip):

it may actually make it harder to debug :) --

nikomatsakis (Nov 01 2019 at 16:14, on Zulip):

the problem there is that we are generating too many subgoals

nikomatsakis (Nov 01 2019 at 16:15, on Zulip):

(maybe I'll try to look at that a bit more later on...)

nikomatsakis (Nov 01 2019 at 16:15, on Zulip):

the stack growth part is just a side-effect from that

Jack Huey (Nov 01 2019 at 16:15, on Zulip):

Ah

Jack Huey (Nov 01 2019 at 16:15, on Zulip):

I briefly skimmed over that conversation, but didn't look closely

Jack Huey (Nov 01 2019 at 16:17, on Zulip):

Importantly, I don't think we lose any debug information with my changes though. Since I call the pursue_strand info_heading for each loop (whereas before it was each recursion)

nikomatsakis (Nov 01 2019 at 16:18, on Zulip):

basically, you made us loop in pursue_strand, instead of having it recursively invoke itself?

good idea though :)

Jack Huey (Nov 01 2019 at 16:19, on Zulip):

Yeah, like I said, it sort of just fell out of the refactoring that I did to make what I was doing simpler

nikomatsakis (Nov 01 2019 at 16:19, on Zulip):

On a related note, I've been wanting to rework the logic that collects cyclic strands into a local vector

nikomatsakis (Nov 01 2019 at 16:19, on Zulip):

so that they are collected instead in the table and we can return back a "QuantumExceeded"

nikomatsakis (Nov 01 2019 at 16:20, on Zulip):

this basically gives the caller more of a chance to interrupt and say "you know what, I don't care that much"

nikomatsakis (Nov 01 2019 at 16:20, on Zulip):

(i.e., it lets them implement "fuel")

Jack Huey (Nov 01 2019 at 16:21, on Zulip):

Yeah, I did a little bit of tinkering with that at the start, but it ended up being mostly unnecessary for this change

Jack Huey (Nov 01 2019 at 16:22, on Zulip):

but definitely worth rethinking

Jack Huey (Nov 05 2019 at 01:33, on Zulip):

@nikomatsakis Okay, I've updated the PR for your comments

Jack Huey (Nov 05 2019 at 01:34, on Zulip):

I also went through and verified that no subgoals can be added when allow_coinductive is true

Jack Huey (Nov 05 2019 at 01:36, on Zulip):

See my github comment, but basically they are really only added in push_initial_strands_instantiated, which I would sort of expect

Jack Huey (Nov 05 2019 at 01:38, on Zulip):

Also, I've done some more cleanup/refactoring in my branch that removes CanonicalStrands. Some of it touches this code, but I'll either just make a separate PR for those or just lump it in with the remove CanonicalStrand PR

Jack Huey (Nov 06 2019 at 19:31, on Zulip):

@nikomatsakis For your second suspicion, is that only in the context of coinduction or a more general problem?

nikomatsakis (Nov 08 2019 at 10:41, on Zulip):

@Jack Huey I apologize for radio silence, I'm not sure what's been going on last few weeks but I've been very short of time. I'm skimming your branch now. I am starting to wonder if it'd be a good idea to factor out some of the cleanup work and land it separately, just to help concentrate the diff

nikomatsakis (Nov 08 2019 at 10:42, on Zulip):

The code which propagates the CanonicalStrand out of ensure_answer feels... I'm not sure. Similar-ish to what I initially had in mind, but somehow more complicated.

Actually maybe it's a good idea for me to try to be more precise about what I had in mind, so I can compare it to what you have done. I've been doing this in my head but I've not written it down in detail.

nikomatsakis (Nov 08 2019 at 10:43, on Zulip):

In short, what I had in mind was:

nikomatsakis (Nov 08 2019 at 10:43, on Zulip):

When a cycle occurs, we would take the goal and add it to a list in the Strand, let's call it delayed_coinductive_subgoals -- this is basically what you did to start.

nikomatsakis (Nov 08 2019 at 10:44, on Zulip):

But then, when the other subgoals have (successfully) completed, I was imagining we would produce an answer, but that answer would include the delayed subgoals as well (effectively like the old delayed literals)

nikomatsakis (Nov 08 2019 at 10:45, on Zulip):

But when you incorporate the answer from another table, if it was delayed on yourself, you would remove that goal

nikomatsakis (Nov 08 2019 at 10:45, on Zulip):

There would ultimately have to be a loop much like the one you've added

nikomatsakis (Nov 08 2019 at 10:45, on Zulip):

i.e., ensure_root_answer, if it gets back an answer with a delayed goal, would have to do a search

nikomatsakis (Nov 08 2019 at 10:45, on Zulip):

so maybe this code is kind of equivalent

Jack Huey (Nov 08 2019 at 15:14, on Zulip):

@nikomatsakis No problem.

Jack Huey (Nov 08 2019 at 15:14, on Zulip):

So, with your approach

Jack Huey (Nov 08 2019 at 15:15, on Zulip):

the difference is mostly in where we "store" the "delayed subgoal"

Jack Huey (Nov 08 2019 at 15:15, on Zulip):

I think

nikomatsakis (Nov 08 2019 at 15:17, on Zulip):

@Jack Huey this morning while making breakfast I think I saw how to describe my proposal

nikomatsakis (Nov 08 2019 at 15:17, on Zulip):

but didn't haev time to write it down yet

nikomatsakis (Nov 08 2019 at 15:17, on Zulip):

I will try to do that after compiler meeting

nikomatsakis (Nov 08 2019 at 15:17, on Zulip):

But I was thinking, are youa ble to attend trait design meeting on Monday?

Jack Huey (Nov 08 2019 at 15:17, on Zulip):

No problem

nikomatsakis (Nov 08 2019 at 15:17, on Zulip):

Maybe we should make this the topic?

nikomatsakis (Nov 08 2019 at 15:18, on Zulip):

(Which wouldn't preclude you messing about with it, just seems like a good thing to discuss more broadly)

nikomatsakis (Nov 08 2019 at 15:18, on Zulip):

I'd like to use those meetings to focus on work people are doing as much as possible, to help spread understanding

Jack Huey (Nov 08 2019 at 15:18, on Zulip):

Sure, I'll be around

Jack Huey (Nov 08 2019 at 15:18, on Zulip):

I'll also split out the refactoring-type stuff into a separate PR. That doesn't change anything

nikomatsakis (Nov 08 2019 at 15:18, on Zulip):

that would be great

Jack Huey (Nov 08 2019 at 15:19, on Zulip):

As you can see, I also have the changes to remove CanonicalStrand ready

Jack Huey (Nov 08 2019 at 15:19, on Zulip):

(and have been working on the "fuel friendly" issue)

nikomatsakis (Nov 08 2019 at 15:20, on Zulip):

the short version of what I had in mind is:

ok, have to go back to other meeting ;)

nikomatsakis (Nov 08 2019 at 15:20, on Zulip):

maybe that makes sense to you

Jack Huey (Nov 08 2019 at 15:20, on Zulip):

Yes, that was mostly the sense I was getting, so that makes sense

Jack Huey (Nov 08 2019 at 15:20, on Zulip):

I'll try it

nikomatsakis (Nov 08 2019 at 15:54, on Zulip):
* but if you then query a subtable, and the answer has deferred subclauses, we need to "resume" that work, but it should be quick, and we can overwrite the answer in place

a few more notes on this:

I was thinking we could extend pursue_strand so that it takes the index where the index where the answer should be stored. Normally this would be one past the end (i.e., make a new answer). but if we are in ensure_root_answer and we get back answer with deferred subclauses, then we would create a new strand just solving those clauses and tell it to re-execute and overwrite the answer in place.

It is possible that this strand will fail -- in that case, we need to have a way to indicate that an answer was invalidated, and now represents just a failed path.

If you were to later invoke ensure_answer on a failed path, you get back some result that says "failed, but try the next answer".

Jack Huey (Nov 08 2019 at 16:18, on Zulip):

Err. You lost me.

Jack Huey (Nov 08 2019 at 16:18, on Zulip):

I'll have to think about that

Jack Huey (Nov 08 2019 at 16:28, on Zulip):

@nikomatsakis https://github.com/rust-lang/chalk/pull/279

Jack Huey (Nov 08 2019 at 16:28, on Zulip):

A PR with only recursion refactor changes

nikomatsakis (Nov 08 2019 at 16:30, on Zulip):

@Jack Huey I started a hackmd document summarizing what's going on, as a draft for meeting

nikomatsakis (Nov 08 2019 at 16:31, on Zulip):

nikomatsakis For your second suspicion, is that only in the context of coinduction or a more general problem?

I also added an example illustrating the case I was suspicious about

nikomatsakis (Nov 08 2019 at 16:31, on Zulip):

it is only a problem for coinduction, not a more general problem, the rest of the code should handle it just fine

Jack Huey (Nov 08 2019 at 16:34, on Zulip):

Ok I'll take a look

nikomatsakis (Nov 08 2019 at 16:40, on Zulip):

Err. You lost me.

that last part is kind of an optimization, not that imp't

nikomatsakis (Nov 08 2019 at 16:52, on Zulip):

let more notes in the hackmd, gotta run

Jack Huey (Nov 08 2019 at 16:52, on Zulip):

@nikomatsakis Looking at the unification example you gave, I don't think my branch would handle that

Jack Huey (Nov 08 2019 at 17:03, on Zulip):

Actually, I wrote a test for it. And (assuming my test is correct), it passes

Jack Huey (Nov 08 2019 at 18:04, on Zulip):

Ok, changing my test a bit reveals that while branch doesn't necessarily give a wrong answer, it does Flounder when it could give NoSolutions

Jack Huey (Nov 08 2019 at 21:39, on Zulip):

@nikomatsakis Should I just got ahead and add back Stacker, but just wrap the pursue_next_strand call in ensure_answer_recursively?

nikomatsakis (Nov 08 2019 at 21:40, on Zulip):

seems good -- or wrap calls to ensure_answer_recursively

nikomatsakis (Nov 08 2019 at 21:40, on Zulip):

but yeah basically when we enter into ensure-answer

nikomatsakis (Nov 08 2019 at 21:40, on Zulip):

well, we only want to wrap one spot

nikomatsakis (Nov 08 2019 at 21:40, on Zulip):

I think your first suggestion was correct

Jack Huey (Nov 08 2019 at 21:42, on Zulip):

Ok I'll do that

Jack Huey (Nov 08 2019 at 21:44, on Zulip):

Also, the remove CanonicalStrand PR should be fairly straightforward too, I think

Jack Huey (Nov 08 2019 at 21:45, on Zulip):

@nikomatsakis PR is updated

nikomatsakis (Nov 09 2019 at 13:06, on Zulip):

@Jack Huey ok, I've convinced myself that my coinduction scheme seems good -- but I've got to dig a bit more into the PR now with that revised understanding still

Jack Huey (Nov 09 2019 at 13:27, on Zulip):

Sure! The PR definitely doesn't handle the cases you brought up correctly

Jack Huey (Nov 09 2019 at 13:28, on Zulip):

I added tests for them

Jack Huey (Nov 11 2019 at 18:22, on Zulip):

I've maybe like 70% implemented your coinductive approach

Jack Huey (Nov 11 2019 at 18:29, on Zulip):

The only test not passing (including the new tests covering some of the new cases + removing the fixme on the existing test) is test::wf_lowering::cyclic_wf_requirements

Jack Huey (Nov 11 2019 at 18:29, on Zulip):

But I need to add your variant 2 and 3 as tests

Jack Huey (Nov 11 2019 at 18:29, on Zulip):

I think those will fail

Jack Huey (Nov 11 2019 at 20:25, on Zulip):

Oops I was adding delayed_subgoals when incoporating an answer into delayed_subgoals instead of subgoals

Jack Huey (Nov 11 2019 at 20:25, on Zulip):

Which exposes a different problem :)

nikomatsakis (Nov 11 2019 at 20:49, on Zulip):

yeah that's not right :)

Jack Huey (Nov 11 2019 at 21:27, on Zulip):

@nikomatsakis ok, I'm maybe a bit stuck and have a question

Jack Huey (Nov 11 2019 at 21:27, on Zulip):

Still stuck on the same cyclic_wf_requirements test

nikomatsakis (Nov 11 2019 at 21:28, on Zulip):

what's up

Jack Huey (Nov 11 2019 at 21:28, on Zulip):

One of the tables is returning an answer with a delayed subgoal of InEnvironment { environment: Env([FromEnv(Unit)]), goal: WellFormed(<?0 as Foo>::Value: Foo) }

Jack Huey (Nov 11 2019 at 21:29, on Zulip):

Now, I feel like I need to do some sort of canonicalization somewhere that I'm not doing

Jack Huey (Nov 11 2019 at 21:30, on Zulip):

(I think this isn't correct, so I'm about to look more into this, but want to actually fully type of the problem in case you have insight) But InEnvironment { environment: Env([FromEnv(Unit)]), goal: WellFormed(<Unit as Foo>::Value: Foo) } is getting pushed as a subgoal for the next strand up

Jack Huey (Nov 11 2019 at 21:31, on Zulip):

but then truncating that goal panics

nikomatsakis (Nov 11 2019 at 21:31, on Zulip):

this may be because ?0 is an inference variable that got unified with Unit

nikomatsakis (Nov 11 2019 at 21:31, on Zulip):

depending on where you are printing the value

nikomatsakis (Nov 11 2019 at 21:31, on Zulip):

it may not reflect all the unifications that happened

nikomatsakis (Nov 11 2019 at 21:32, on Zulip):

I guess if you have a branch (or a "Draft" PR) that might be helpful

Jack Huey (Nov 11 2019 at 21:32, on Zulip):

oh wait no. it's normalize_deep that's panicing

Jack Huey (Nov 11 2019 at 21:33, on Zulip):

Sure I'll just push my changes to the same PR?

nikomatsakis (Nov 11 2019 at 21:34, on Zulip):

which PR?

nikomatsakis (Nov 11 2019 at 21:34, on Zulip):

seems ok

Jack Huey (Nov 11 2019 at 21:35, on Zulip):

The coinduction PR

Jack Huey (Nov 11 2019 at 21:35, on Zulip):

since I don't think we're going with the implementation I had

Jack Huey (Nov 11 2019 at 21:35, on Zulip):

though I'll keep it as a branch

Jack Huey (Nov 11 2019 at 21:36, on Zulip):

Ok https://github.com/rust-lang/chalk/pull/272 has the changes

Jack Huey (Nov 11 2019 at 21:55, on Zulip):

Oh shoot I got it to work

Jack Huey (Nov 11 2019 at 21:56, on Zulip):

I don't know if it's necessarily the right thing (probably isn't)

Jack Huey (Nov 11 2019 at 21:56, on Zulip):

and a couple tests fail so

Jack Huey (Nov 11 2019 at 21:57, on Zulip):

but I ended up canonicalizing the goal before storing it in the delayed_subgoals

Jack Huey (Nov 11 2019 at 22:18, on Zulip):

Oh

Jack Huey (Nov 11 2019 at 22:18, on Zulip):

So

Jack Huey (Nov 11 2019 at 22:18, on Zulip):
[chalk-engine/src/logic.rs:1046] &delayed_subgoal = UCanonical {
    canonical: Canonical {
        value: InEnvironment {
            environment: Env([FromEnv(Unit)]),
            goal: WellFormed(<Unit as Foo>::Value: Foo),
        },
        binders: [],
    },
    universes: 1,
}
[chalk-engine/src/logic.rs:1047] &table_goal = UCanonical {
    canonical: Canonical {
        value: InEnvironment {
            environment: Env([FromEnv(Unit)]),
            goal: WellFormed(Unit: Foo),
        },
        binders: [],
    },
    universes: 1,
}
Jack Huey (Nov 11 2019 at 22:19, on Zulip):

Those are the same

Jack Huey (Nov 11 2019 at 22:19, on Zulip):

So my "trivial self-cycle" check is not taking into account normalization

Jack Huey (Nov 11 2019 at 22:58, on Zulip):

Ok @nikomatsakis I left some comments on the PR with some questions/comments

nikomatsakis (Nov 11 2019 at 23:39, on Zulip):

ok @Jack Huey will try to look soon!

Jack Huey (Nov 12 2019 at 04:55, on Zulip):

Ok a few thoughts:

Jack Huey (Nov 12 2019 at 04:56, on Zulip):

1) Are auto traits supposed to be non-enumerable or not? If so, how does this play into everything?

Jack Huey (Nov 12 2019 at 04:59, on Zulip):

(From what I can tell, removing the check for auto traits in program_clauses and the panic in program_clauses_that_could_match causes a few tests to return [] instead of Flounder irt. auto traits, but otherwise is fine.)

Jack Huey (Nov 12 2019 at 05:00, on Zulip):

(When making these changes coinductive_conflicting2 test passes)

Jack Huey (Nov 12 2019 at 05:01, on Zulip):

2) My coinductive_conflicting3 test still fails with the above changes, but because it finds a unique solution with T=B. The T=A subst isn't getting added to the T: C1 table

nikomatsakis (Nov 12 2019 at 14:44, on Zulip):

1) Are auto traits supposed to be non-enumerable or not? If so, how does this play into everything?

Are, yeah, a good question. I think that yes, auto traits are non-enumerable, more so than any other trait really. Probably we want to say that all traits are non-enumerable

Jack Huey (Nov 12 2019 at 20:11, on Zulip):

Probably we want to say that all traits are non-enumerable

@nikomatsakis that's a bold statement

Jack Huey (Nov 12 2019 at 20:11, on Zulip):

How does that effect things?

nikomatsakis (Nov 12 2019 at 20:11, on Zulip):

that's what rustc does, at least

nikomatsakis (Nov 12 2019 at 20:11, on Zulip):

it doesn't really matter to the engine at all?

Jack Huey (Nov 12 2019 at 20:12, on Zulip):

Well, it does sort of

nikomatsakis (Nov 12 2019 at 20:12, on Zulip):

Why do you think so?

nikomatsakis (Nov 12 2019 at 20:12, on Zulip):

Because it affects some tests?

nikomatsakis (Nov 12 2019 at 20:12, on Zulip):

Or is there some other reason

Jack Huey (Nov 12 2019 at 20:12, on Zulip):

Actually, I guess the part that cares here isn't actually in chalk-engine

Jack Huey (Nov 12 2019 at 20:13, on Zulip):

But

Jack Huey (Nov 12 2019 at 20:14, on Zulip):

chalk-solve is Floundering a table in program_clausesfor non-enumerable types

nikomatsakis (Nov 12 2019 at 20:14, on Zulip):

seems ok

Jack Huey (Nov 12 2019 at 20:14, on Zulip):

so even though we can prove that something isn't possible, it flounders

Jack Huey (Nov 12 2019 at 20:14, on Zulip):

(also for auto traits)

nikomatsakis (Nov 12 2019 at 20:14, on Zulip):

how can we prove it's not possible?

Jack Huey (Nov 12 2019 at 20:15, on Zulip):

So, this was one of your examples

Jack Huey (Nov 12 2019 at 20:15, on Zulip):

one sec

Jack Huey (Nov 12 2019 at 20:15, on Zulip):
C1(X) :- C2(Y), X = 22.
C2(X) :- C3(X), X = 44.
C3(X) :- C1(X), C2(X).
nikomatsakis (Nov 12 2019 at 20:15, on Zulip):

I see

nikomatsakis (Nov 12 2019 at 20:15, on Zulip):

Yeah, we may not be able to exercise that code path

nikomatsakis (Nov 12 2019 at 20:16, on Zulip):

Without some "opt-in" to enumerating rules

Jack Huey (Nov 12 2019 at 20:16, on Zulip):

The test is here: https://github.com/rust-lang/chalk/pull/272/files#diff-721709466568566f24fc2e8634c40dcbR140

nikomatsakis (Nov 12 2019 at 20:16, on Zulip):

Really we don't want auto-traits for these tests

nikomatsakis (Nov 12 2019 at 20:16, on Zulip):

We just want a way to write "coinductive" traits

nikomatsakis (Nov 12 2019 at 20:16, on Zulip):

maybe we should enable that

nikomatsakis (Nov 12 2019 at 20:16, on Zulip):

auto-traits come with other baggage (i.e., implemented for all structs, etc)

Jack Huey (Nov 12 2019 at 20:16, on Zulip):

Hmm

Jack Huey (Nov 12 2019 at 20:16, on Zulip):

is there a separate way to mark a trait as coinductive only

Jack Huey (Nov 12 2019 at 20:18, on Zulip):

Right now, a goal is coinductive if 1) We ask if an auto trait is implemented or 2) It's a well-formed goal

nikomatsakis (Nov 12 2019 at 20:33, on Zulip):

is there a separate way to mark a trait as coinductive only

no, but we could add one

nikomatsakis (Nov 12 2019 at 20:34, on Zulip):

it would require a bit of threading

nikomatsakis (Nov 12 2019 at 20:34, on Zulip):

we'd add a #[coinductive] attribute or something

nikomatsakis (Nov 12 2019 at 20:34, on Zulip):

I've sometimes wondered if we can make all traits coinductive, but anyway

Jack Huey (Nov 12 2019 at 20:34, on Zulip):

Yeah, I was curious about that

Jack Huey (Nov 12 2019 at 20:35, on Zulip):

So, is it worth adding that? If so, in this PR or in a separate one? Otherwise, can't really test these two cases

Jack Huey (Nov 12 2019 at 20:35, on Zulip):

(at least, can't test that they go to no solution instead of floundering)

Jack Huey (Nov 12 2019 at 21:15, on Zulip):

It was easy enough to add and better tests the minimal "only coinductive" behavior we want to test so I added it

Jack Huey (Nov 12 2019 at 21:15, on Zulip):

And all the tests (for coinductiveness), so far, pass

Jack Huey (Nov 12 2019 at 21:15, on Zulip):

The coinductive_semantics test is actually and auto_semantics test

Jack Huey (Nov 12 2019 at 21:16, on Zulip):

(deleted)

Jack Huey (Nov 12 2019 at 21:22, on Zulip):

@nikomatsakis I have maybe a naive question

Jack Huey (Nov 12 2019 at 21:22, on Zulip):

C1(A, B) :- C1(B, A).

Jack Huey (Nov 12 2019 at 21:22, on Zulip):

I'm not exactly sure what haven't two variables here means

Jack Huey (Nov 12 2019 at 21:23, on Zulip):

So C1(A) :- C2(A) means A: C1 if A: C2

nikomatsakis (Nov 12 2019 at 21:56, on Zulip):

@Jack Huey you could model it as (A, B): C1, for example, or as A: C1<B>

Jack Huey (Nov 12 2019 at 22:28, on Zulip):

Oh, that's good to know

Jack Huey (Nov 13 2019 at 16:21, on Zulip):

@nikomatsakis just wondering if you've gotten a chance to take a look at the coinductive PR?

nikomatsakis (Nov 14 2019 at 01:51, on Zulip):

not today, will try to do that tomorrow @Jack Huey

Jack Huey (Nov 14 2019 at 01:51, on Zulip):

No problem

Jack Huey (Nov 14 2019 at 01:52, on Zulip):

I realized that I'm sort of in a dilemma with it

nikomatsakis (Nov 14 2019 at 10:34, on Zulip):

@Jack Huey does this have to do you with your latest comment about floundering, or something else?

nikomatsakis (Nov 14 2019 at 10:36, on Zulip):

(To start, I think we should rebase the "coinductive" attribute and land that, btw)

nikomatsakis (Nov 14 2019 at 10:38, on Zulip):

OK, reading branch now. I'm going to try making a few edits and push to the branch, hope you don't mind. I just don't think i'll have much time today and this seems like fastest way to give feedback.

nikomatsakis (Nov 14 2019 at 10:53, on Zulip):

OK, that may have been ambitious on my part. The main bit of feedback is that indeed the delayed subgoals have to be canonicalized together with the answer substitution. This implies that I think we have to add another associated type besides CanonicalConstrainedSubst -- I was trying to add one entitled CanonicalAnswerSubst, which would include the delayed subgoals. I am pondering where the delayed subgoals should be introduced to the ex-clause -- probably as part of apply_answer_subst, though I think that this code cannot really be expected to detect trivial-self-cycles... well, I guess why not? it already knows the goal.

nikomatsakis (Nov 14 2019 at 10:54, on Zulip):

As a crazy nit-pick, I was tempted to suggest that CompleteAnswer should just be Answer, and that Answer should be PartialAnswer or something, but I'm not really sure if I like that. =)

nikomatsakis (Nov 14 2019 at 10:55, on Zulip):

Ah yeah and the ExClause should not be storing canonical goals, just uncanonical ones

nikomatsakis (Nov 14 2019 at 11:08, on Zulip):

well, I pushed a commit that starts going down that road, but it's not complete

Jack Huey (Nov 14 2019 at 14:57, on Zulip):

@nikomatsakis thanks for the feedback! I'll try to take the changes that you made and run with it

Jack Huey (Nov 14 2019 at 17:58, on Zulip):

https://github.com/rust-lang/chalk/pull/285

Jack Huey (Nov 14 2019 at 17:58, on Zulip):

PR with just coinductive attribute + new tests

Jack Huey (Nov 15 2019 at 20:47, on Zulip):

@nikomatsakis you around?

Jack Huey (Nov 15 2019 at 20:47, on Zulip):

Question

Jack Huey (Nov 15 2019 at 20:47, on Zulip):

So, when we get non-trivial self-cycle subgoals in the answer for the root goal, those are C::GoalInEnvironment

Jack Huey (Nov 15 2019 at 20:48, on Zulip):

If we want to reevaluate those, they need to be C::UCanonicalGoalInEnvironment

Jack Huey (Nov 15 2019 at 20:48, on Zulip):

what's the correct way to convert that

nikomatsakis (Nov 16 2019 at 10:14, on Zulip):

I'm not sure I understand the question yet

nikomatsakis (Nov 16 2019 at 10:15, on Zulip):

Something seems wrong @Jack Huey -- do you mean from evaluate_root_goal (or wherever we do the "answer refinement" stage)?

nikomatsakis (Nov 16 2019 at 10:17, on Zulip):

I think the idea would be to make a strand within that same table, and I think it should only need goals

nikomatsakis (Nov 16 2019 at 10:17, on Zulip):

Have you pushed to the PR?

Jack Huey (Nov 16 2019 at 20:04, on Zulip):

@nikomatsakis Yes I mean in ensure_root_answer (which I just renamed to root_answer and return the CompleteAnswer.

Jack Huey (Nov 16 2019 at 20:05, on Zulip):

Anyways, I ended up figuring it out

Jack Huey (Nov 16 2019 at 20:05, on Zulip):

and all the tests pass

Jack Huey (Nov 16 2019 at 20:05, on Zulip):

But, the way I approach is may not be (probably not) 100%

Jack Huey (Nov 16 2019 at 20:06, on Zulip):

Basically, in short, the "answer" for the root table may have non-trivial self-cycles as delayed subgoals

Jack Huey (Nov 16 2019 at 20:06, on Zulip):

But there are C::GoalInEnvironment

Jack Huey (Nov 16 2019 at 20:06, on Zulip):

If we want to try to evaluate these, we need a C::UCanonicalGoalInEnvironment

Jack Huey (Nov 16 2019 at 20:08, on Zulip):

I ended up just making a new function in Context which takes the UCanonicalGoalInEnvironment from the root goal and applies it's binders to the GoalInEnvironment for the delayed_subgoal

Jack Huey (Nov 16 2019 at 20:09, on Zulip):

Which I don't think is necessarily the correct way to do it. But it does work, at least for the current tests

Jack Huey (Nov 16 2019 at 20:09, on Zulip):

So,

Jack Huey (Nov 16 2019 at 20:09, on Zulip):

I'll clean up my changes locally and push to the PR for comments/review

Jack Huey (Nov 16 2019 at 20:16, on Zulip):

There's also other "assumptions" I've made currently that I don't think will always hold (but do for current tests), once I push these changes I'm gonna work on making some tests that break these

nikomatsakis (Nov 18 2019 at 18:39, on Zulip):

@Jack Huey I took a peek at the commits so far, will do a more in-depth look later

Jack Huey (Nov 18 2019 at 18:40, on Zulip):

@nikomatsakis Any (general) comments?

nikomatsakis (Nov 18 2019 at 18:40, on Zulip):

Not yet, it seemed "pretty close" -- the logic around what is a "trivial cycle" probably needs a bit of tweaking -- but yeah

Jack Huey (Nov 18 2019 at 18:40, on Zulip):

Ok

Jack Huey (Nov 18 2019 at 18:43, on Zulip):

The big thing right now I personally am unsure about are whether the way I'm handling the binders for delayed subgoals

Jack Huey (Nov 18 2019 at 18:44, on Zulip):

And I guess, in what cases might we have a substitution from a delayed subgoal and how do we incorporate that

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

@nikomatsakis I'll have to update the branch to fix the new merge conflict from yesterday, but do you think you'll have time this week to review the coinduction branch?

nikomatsakis (Dec 10 2019 at 21:58, on Zulip):

@Jack Huey yes

nikomatsakis (Dec 13 2019 at 14:02, on Zulip):

@Jack Huey I've been looking it over. One thing that might be worth talking about -- perhaps as a standalone PR and a "pre-step" -- is having a mechanism to "invalidate" previous answers as having been superceded by newer ones. You remember how we were talking about what to do for https://github.com/rust-lang/chalk/issues/302.

Jack Huey (Dec 13 2019 at 17:12, on Zulip):

So, unless I'm mistaken, for this it wouldn't actually do anything except maybe be a performance optimization?

nikomatsakis (Dec 13 2019 at 17:26, on Zulip):

in some sense that's always true

nikomatsakis (Dec 13 2019 at 17:29, on Zulip):

anyway, let me poke at this branch a bit

Jack Huey (Dec 13 2019 at 17:29, on Zulip):

Also, I think the answer invalidation in that issue is different than what would be used for conduction

Jack Huey (Dec 13 2019 at 17:30, on Zulip):

Maybe

nikomatsakis (Dec 13 2019 at 17:31, on Zulip):

I don't think so

nikomatsakis (Dec 13 2019 at 17:31, on Zulip):

basically just a way to say "there's a better answer later"

nikomatsakis (Dec 13 2019 at 17:32, on Zulip):

or rather "this 'answer' turned out to be an error"

nikomatsakis (Dec 13 2019 at 17:32, on Zulip):

but I don't think it's really a necessary pre-step, thinking more about it

Jack Huey (Dec 13 2019 at 17:33, on Zulip):

Tbh thinking about an "answer turning out to be an error" sounds scary

nikomatsakis (Dec 13 2019 at 17:34, on Zulip):

heh

Jack Huey (Dec 13 2019 at 17:34, on Zulip):

I'm also not sure if the technical overhead is really worth whatever performance difference

nikomatsakis (Dec 13 2019 at 17:34, on Zulip):

it's not so scary as it sounds

nikomatsakis (Dec 13 2019 at 17:35, on Zulip):

like, if an answer includes delayed subgoals, then it's clear that an "answer" can lead to an error

nikomatsakis (Dec 13 2019 at 17:35, on Zulip):

(i.e., processing those subgoals can fail)

nikomatsakis (Dec 13 2019 at 17:35, on Zulip):

anyway, we can revisit after, I agree it's not a necessary step

nikomatsakis (Dec 13 2019 at 17:51, on Zulip):

@Jack Huey do you happen to have that hackmd handy where we worked through the algorithm? I think I may see an opportunity for simplification here actually..

nikomatsakis (Dec 13 2019 at 17:51, on Zulip):

I guess it was probably this one

Jack Huey (Dec 13 2019 at 17:54, on Zulip):

Yep that's it

nikomatsakis (Dec 13 2019 at 17:56, on Zulip):

And indeed it points out to me why the simplification doesn't work

nikomatsakis (Dec 13 2019 at 17:56, on Zulip):

Though I think there's still a simpler way to express things than the way I explained it in the doc

Jack Huey (Dec 13 2019 at 17:57, on Zulip):

In what way?

Jack Huey (Dec 13 2019 at 17:58, on Zulip):

Did i do something wrong

nikomatsakis (Dec 13 2019 at 17:59, on Zulip):

let me try to "prove out" this real quick

nikomatsakis (Dec 13 2019 at 18:00, on Zulip):

before I respond

Jack Huey (Dec 13 2019 at 18:01, on Zulip):

Sure

nikomatsakis (Dec 13 2019 at 18:21, on Zulip):

Ok @Jack Huey I pushed some commits to your branch

nikomatsakis (Dec 13 2019 at 18:21, on Zulip):

the key idea is this:

nikomatsakis (Dec 13 2019 at 18:21, on Zulip):

when -- in the root table --

nikomatsakis (Dec 13 2019 at 18:21, on Zulip):

we publish an answer A :- B | with delayed subgoals B

nikomatsakis (Dec 13 2019 at 18:21, on Zulip):

we immediately create a new strand in that table A :- B

nikomatsakis (Dec 13 2019 at 18:22, on Zulip):

(the logic for doing that is perhaps mildly inefficient right now in its treatment of canonicalization)

nikomatsakis (Dec 13 2019 at 18:23, on Zulip):

we can still consider the original answer valid; I marked it as ambiguous for now but I think that's not quite right, as my comment explains

nikomatsakis (Dec 13 2019 at 18:23, on Zulip):

I haven't of course tried to test this :)

Jack Huey (Dec 13 2019 at 18:26, on Zulip):

That's an interesting approach

Jack Huey (Dec 13 2019 at 18:27, on Zulip):

And that could mean that replacing a previous answer is needed?

nikomatsakis (Dec 13 2019 at 18:27, on Zulip):

well so

nikomatsakis (Dec 13 2019 at 18:28, on Zulip):

actually I think we should just consider the previous answer -- when it propagates out from the table -- as an error

nikomatsakis (Dec 13 2019 at 18:28, on Zulip):

because this follow-up strand will publish another one that is better

nikomatsakis (Dec 13 2019 at 18:28, on Zulip):

but that was not really what I originally had in mind, at least not exactly

Jack Huey (Dec 13 2019 at 18:28, on Zulip):

I feel like the aggregator won't handle this correctly?

nikomatsakis (Dec 13 2019 at 18:29, on Zulip):

ah, yeah, I think that's corect, I had planned to remove that logic

nikomatsakis (Dec 13 2019 at 18:29, on Zulip):

I mean I think it's wrong for it to panic anyway

nikomatsakis (Dec 13 2019 at 18:29, on Zulip):

well I know that's wrong

nikomatsakis (Dec 13 2019 at 18:29, on Zulip):

but then the question is what to do instead :)

Jack Huey (Dec 13 2019 at 18:29, on Zulip):

Well that too. But also

nikomatsakis (Dec 13 2019 at 18:29, on Zulip):

er, sorry, you meant the answer aggregator

Jack Huey (Dec 13 2019 at 18:29, on Zulip):

If the first answer is ambiguous

nikomatsakis (Dec 13 2019 at 18:30, on Zulip):

yeah this is why ambiguous is not correct

nikomatsakis (Dec 13 2019 at 18:30, on Zulip):

although

Jack Huey (Dec 13 2019 at 18:30, on Zulip):

Then we can no longer get a unique answer

nikomatsakis (Dec 13 2019 at 18:30, on Zulip):

that's not true

nikomatsakis (Dec 13 2019 at 18:30, on Zulip):

I'm not sure what the aggregator will do but

nikomatsakis (Dec 13 2019 at 18:30, on Zulip):

if you have two answers with the same substitution

nikomatsakis (Dec 13 2019 at 18:30, on Zulip):

and one is ambiguous and the other not

nikomatsakis (Dec 13 2019 at 18:30, on Zulip):

you can ignore the ambiguous one

Jack Huey (Dec 13 2019 at 18:30, on Zulip):

I was running into this with the associated types branch

nikomatsakis (Dec 13 2019 at 18:30, on Zulip):

but likely the aggregator is not smart enough

Jack Huey (Dec 13 2019 at 18:31, on Zulip):

The aggregator assumes the answers can't unify

nikomatsakis (Dec 13 2019 at 18:31, on Zulip):

and in any case the other consideration is when the refinement strand just outright fails

nikomatsakis (Dec 13 2019 at 18:31, on Zulip):

in which case the first answer isn't ambiguous, it's just false

Jack Huey (Dec 13 2019 at 18:31, on Zulip):

So it makes the most generic form it can

nikomatsakis (Dec 13 2019 at 18:31, on Zulip):

well it assumes that if they are different, yes

nikomatsakis (Dec 13 2019 at 18:31, on Zulip):

anyway it's pretty dumb

nikomatsakis (Dec 13 2019 at 18:31, on Zulip):

but I think really it shouldn't even be seeing the first answer

nikomatsakis (Dec 13 2019 at 18:31, on Zulip):

I don't think there's any info to be gained from it

nikomatsakis (Dec 13 2019 at 18:32, on Zulip):

(at least in this case)

Jack Huey (Dec 13 2019 at 18:32, on Zulip):

Right, which is why I did the refinement before returning a root answer

nikomatsakis (Dec 13 2019 at 18:32, on Zulip):

yeah but

nikomatsakis (Dec 13 2019 at 18:32, on Zulip):

it's easier to

nikomatsakis (Dec 13 2019 at 18:32, on Zulip):

just return a marker value

nikomatsakis (Dec 13 2019 at 18:32, on Zulip):

that's like "ignore me, find the next answer"

Jack Huey (Dec 13 2019 at 18:33, on Zulip):

Actually, this is where I think maybe the non-recursive changes can help us

nikomatsakis (Dec 13 2019 at 18:33, on Zulip):

(conceptually the aggregator could even just ignore answers that have delayed subgoals, but I think it's somehow cleaner to hide that detail from outside the table)

Jack Huey (Dec 13 2019 at 18:33, on Zulip):

I haven't thought a ton about it yet

nikomatsakis (Dec 13 2019 at 18:33, on Zulip):

hmm I don't see what they have to do with it :)

Jack Huey (Dec 13 2019 at 18:34, on Zulip):

But I think it should be clean enough to refine before returning

nikomatsakis (Dec 13 2019 at 18:34, on Zulip):

you cannot refine before returning

nikomatsakis (Dec 13 2019 at 18:34, on Zulip):

well

nikomatsakis (Dec 13 2019 at 18:34, on Zulip):

what I mean is

nikomatsakis (Dec 13 2019 at 18:34, on Zulip):

unless you want to have two distinct sets of answer indices

nikomatsakis (Dec 13 2019 at 18:34, on Zulip):

the first answer is real, and has to be in the table

nikomatsakis (Dec 13 2019 at 18:34, on Zulip):

unless maybe you are thinking to overwrite it in place

nikomatsakis (Dec 13 2019 at 18:35, on Zulip):

but I don't think it's actually that clean

Jack Huey (Dec 13 2019 at 18:35, on Zulip):

Hmm

nikomatsakis (Dec 13 2019 at 18:35, on Zulip):

e.g., consider this

nikomatsakis (Dec 13 2019 at 18:35, on Zulip):

the table maybe have other strands that haven't completed yet

nikomatsakis (Dec 13 2019 at 18:35, on Zulip):

and so if we publish an answer X

nikomatsakis (Dec 13 2019 at 18:35, on Zulip):

and then create a strand to refine X

nikomatsakis (Dec 13 2019 at 18:35, on Zulip):

trying to do that could lead to (e.g.) running out of quantum or fuel

nikomatsakis (Dec 13 2019 at 18:36, on Zulip):

it's just a lot of state to juggle

nikomatsakis (Dec 13 2019 at 18:36, on Zulip):

but in this approach, there really is no state

nikomatsakis (Dec 13 2019 at 18:36, on Zulip):

we just say "you're looking for answer N? look for N+1"

nikomatsakis (Dec 13 2019 at 18:36, on Zulip):

which we already have to do

nikomatsakis (Dec 13 2019 at 18:37, on Zulip):

one thing I haven't quite decided yet: could it be that the refinement strand winds up with a different substitution -- or even multiple answers? I guess I have to think about that. Seems...plausible.

Jack Huey (Dec 13 2019 at 18:37, on Zulip):

I'll look over your changes

Jack Huey (Dec 13 2019 at 18:37, on Zulip):

But to answer that question

Jack Huey (Dec 13 2019 at 18:38, on Zulip):

For all current tests...no. I was ignoring that and everything "worked"

nikomatsakis (Dec 13 2019 at 18:38, on Zulip):

I realize I already overlooked one bit of complexity in the "delayed trivial self cycle" walkthrough I did, in that indeed if we publish a new answer (a "refinement answer"), then our refinement strand will try to build on that too -- though it will lead to a duplicate answer, which I guess is ok

Jack Huey (Dec 13 2019 at 18:38, on Zulip):

But I don't know the answer for "all" cases

nikomatsakis (Dec 13 2019 at 18:40, on Zulip):

Maybe I'll try to make a test

nikomatsakis (Dec 13 2019 at 18:40, on Zulip):

in any case, the logic to create a refinement strand is "roughly" what we want

nikomatsakis (Dec 13 2019 at 18:40, on Zulip):

(I think:)

Jack Huey (Dec 13 2019 at 18:43, on Zulip):

I'll take a look at trying to fix the tests

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

Ok @nikomatsakis, I took your changes and worked off of them. So, I don't think making an answer having delayed subgoals be "ambiguous" is the right idea (because the solver doesn't know if it should "consider that"). Instead, I made a new fail "InvalidAnswer". The other issue is now matching the delayed subgoal to the table goal (so it doesn't get added to the ex clause). So, I was checking this in apply_answer_subst, but with the changes you made, the bound variables (I think I got the right name?) in the delayed subgoals get unique inference variables compared to the table goal, so can't check equality. As it is, really they need to be checked after the answer subst is canonicalized (which is now in pursue_answer). For now, to make sure it works, I instead just filter the delayed subgoals in create_refinement_strand, but this is a bit late, because the delayed subgoals are already in the ExClause.

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

Oops that's a big blob of text

nikomatsakis (Dec 16 2019 at 15:26, on Zulip):

@Jack Huey "invalid answer" sounds like exactly what I had in mind -- not sure about the rest yet, have to look maybe at the commit, did you push?

Jack Huey (Dec 16 2019 at 15:27, on Zulip):

Yes it's pushed

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

OK, @Jack Huey, I have to run to something else, but I'll try to look at this later on -- did you have specific questions?

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

Nothing specific

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

I need to spend some time and refactor the bit that I talked about (and has a FIXME), but it works now

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

and tests pass

Last update: Jul 03 2020 at 16:55UTC