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

Last update: Nov 12 2019 at 16:00UTC