Stream: wg-traits

Topic: Removing delayed literals


Jack Huey (Oct 29 2019 at 19:38, on Zulip):

@nikomatsakis If you're around and want to talk about https://github.com/rust-lang/chalk/pull/270, I'm here

nikomatsakis (Oct 29 2019 at 19:38, on Zulip):

I'm around-ish

Jack Huey (Oct 29 2019 at 19:38, on Zulip):

np

nikomatsakis (Oct 29 2019 at 19:38, on Zulip):

going to be doing some reviewing, I think

Jack Huey (Oct 29 2019 at 19:39, on Zulip):

I might try later tonight to see if I can try to remove that branch entirely

Jack Huey (Oct 29 2019 at 19:39, on Zulip):

but it'll require changes elsewhere

Jack Huey (Oct 29 2019 at 19:41, on Zulip):

Basically, what I changed it to is that now when a cycle is detected, it's all the strands are marked as ambiguous. But I think for the majority of tests (since most aren't), a non-ambiguous answer is later found. But I need to double check this

Jack Huey (Oct 29 2019 at 19:41, on Zulip):

I'm also thinking that a lot of this is probably occuring when checked_program is called, rather than actually trying to solve the test

Jack Huey (Oct 29 2019 at 19:42, on Zulip):

The test goal(s), that is

nikomatsakis (Oct 29 2019 at 19:43, on Zulip):

Do you know if the delaying code is ever running?

nikomatsakis (Oct 29 2019 at 19:44, on Zulip):

I think it is not, apart from some specific tests in SLG

nikomatsakis (Oct 29 2019 at 19:44, on Zulip):

(I think that code path doesn't just trigger for cycles, it has to be a negative cycle, and there has to be no other strand that can obtain an answer)

Jack Huey (Oct 29 2019 at 19:44, on Zulip):

The specific branch that you commented does get triggered for 99/146 tests

nikomatsakis (Oct 29 2019 at 19:45, on Zulip):

hmm

nikomatsakis (Oct 29 2019 at 19:45, on Zulip):

that's interesting :)

nikomatsakis (Oct 29 2019 at 19:45, on Zulip):

maybe I'll check it out and see what I'm missing

Jack Huey (Oct 29 2019 at 19:45, on Zulip):

I don't think there was code to actually resolve the delayed_literals though? (maybe I'm misremembering) (I think that was issue #79)

nikomatsakis (Oct 29 2019 at 19:46, on Zulip):

we don't currently have code to "undelay" literals, right

nikomatsakis (Oct 29 2019 at 19:46, on Zulip):

but you are correct that it triggers much more frequently than I realized!

nikomatsakis (Oct 29 2019 at 19:47, on Zulip):

and indeed the errors are part of WF

nikomatsakis (Oct 29 2019 at 19:47, on Zulip):

presumably as part of coherence logic, which uses negative reasoning, but maybe not

nikomatsakis (Oct 29 2019 at 19:48, on Zulip):

OH

nikomatsakis (Oct 29 2019 at 19:48, on Zulip):

I think it may be tied to the "CannotProve" goal?

Jack Huey (Oct 29 2019 at 19:49, on Zulip):

What is that used for again? Is it needed?

nikomatsakis (Oct 29 2019 at 19:50, on Zulip):

Yes, we need it, but that's ok

nikomatsakis (Oct 29 2019 at 19:51, on Zulip):

What I mean is

nikomatsakis (Oct 29 2019 at 19:51, on Zulip):

we are still going to need the notion of "ambiguous strands" that you added

nikomatsakis (Oct 29 2019 at 19:51, on Zulip):

and I expected to use them for CannotProve

nikomatsakis (Oct 29 2019 at 19:51, on Zulip):

we basically use it (in coherence) to force some answers into "unknown" territory

nikomatsakis (Oct 29 2019 at 19:52, on Zulip):

however

nikomatsakis (Oct 29 2019 at 19:52, on Zulip):

it looks like the way I implemented CannotProve

nikomatsakis (Oct 29 2019 at 19:52, on Zulip):

was to make it so that the only way to prove CannotProve was to prove not { CannotProve }, thus (intentionally) inducing a little cycle

nikomatsakis (Oct 29 2019 at 19:52, on Zulip):

you can see this in src/simplify.rs

nikomatsakis (Oct 29 2019 at 19:52, on Zulip):

we can presumably implement it a bit more directly

Jack Huey (Oct 29 2019 at 19:53, on Zulip):

Right, I remember this bit of code

nikomatsakis (Oct 29 2019 at 19:54, on Zulip):

basically we could add another case to push_initial_strands_instantiated

nikomatsakis (Oct 29 2019 at 19:54, on Zulip):

that just adds 1 ambiguous strand for CannotProve

Jack Huey (Oct 29 2019 at 19:56, on Zulip):

Sounds reasonable

Jack Huey (Oct 29 2019 at 19:59, on Zulip):

Actually, just adding ex_clause.ambiguous = true to simplify and removing the cannot_prove goal makes all the tests pass except for the ones that are trying to test the negative cycle

Jack Huey (Oct 29 2019 at 19:59, on Zulip):

(with that branch panicing)

Jack Huey (Oct 29 2019 at 20:00, on Zulip):

err, not quite. example_2_3_EWFS also fails, which is not ambiguous

nikomatsakis (Oct 29 2019 at 20:01, on Zulip):

how does it fail?

nikomatsakis (Oct 29 2019 at 20:02, on Zulip):

oh, that's ok

nikomatsakis (Oct 29 2019 at 20:02, on Zulip):

I mean that is also testing negative cycles

nikomatsakis (Oct 29 2019 at 20:03, on Zulip):

via this rule:

X: W :- ..., not { Y: W }, ...
Jack Huey (Oct 29 2019 at 20:03, on Zulip):
test::slg::contradiction
test::slg::example_2_3_EWFS
test::slg::example_3_3_EWFS
test::slg::negative_answer_ambiguous
test::slg::negative_loop
Jack Huey (Oct 29 2019 at 20:03, on Zulip):

Those are the only tests that fail

nikomatsakis (Oct 29 2019 at 20:03, on Zulip):

yeah, I think those are all the tests that are specifically targeting negative cycles

Jack Huey (Oct 29 2019 at 20:03, on Zulip):

Yep

Jack Huey (Oct 29 2019 at 20:06, on Zulip):

So, rather than panic, should it just return an error?

Jack Huey (Oct 29 2019 at 20:08, on Zulip):

RecursiveSearchFail::NegativeCycle?

Jack Huey (Oct 29 2019 at 20:08, on Zulip):

(does not exist atm)

Jack Huey (Oct 29 2019 at 20:08, on Zulip):

Slightly different than RecursiveSearchFail::Cycle(Minimums)

Jack Huey (Oct 29 2019 at 20:09, on Zulip):

which could be changed to RecursiveSearchFail::PositiveCycle(Minimums)

Jack Huey (Oct 29 2019 at 20:28, on Zulip):

@nikomatsakis Ok, that works. I just added a new enum value NegativeCycle to RecursiveSearchFail RootSearchFail and StrandFail that when encountered fail immediately

Jack Huey (Oct 29 2019 at 20:28, on Zulip):

This just gets changed into None for an answer

nikomatsakis (Oct 29 2019 at 20:28, on Zulip):

I forget what the semantics of None are

nikomatsakis (Oct 29 2019 at 20:28, on Zulip):

but that sounds plausible :)

nikomatsakis (Oct 29 2019 at 20:29, on Zulip):

the reason to panic is that we are supposed to not encounter negative cycles by construction

nikomatsakis (Oct 29 2019 at 20:29, on Zulip):

but I think propagating it out from the core engine

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

Floundered also returns None

nikomatsakis (Oct 29 2019 at 20:29, on Zulip):

to a level more like chalk-solve seems good

nikomatsakis (Oct 29 2019 at 20:29, on Zulip):

yes, ok.

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

yeah, I figured propagating out makes more sense than panicing here

nikomatsakis (Oct 29 2019 at 20:29, on Zulip):

to a level more like chalk-solve seems good

in partcular, it's chalk-solve that would be maintaining this invariant

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

Hmm

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

Ok, so probably add another variant to Solution: NegativeCycle?

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

Or just panic

Jack Huey (Oct 29 2019 at 20:31, on Zulip):

err

Jack Huey (Oct 29 2019 at 20:31, on Zulip):

By then, it's Some(answer) or None

Jack Huey (Oct 29 2019 at 20:34, on Zulip):

Alright so I was wrong. Floundered returns Some(..) with an ambiguous answer. NoMoreSolutions returns None

nikomatsakis (Oct 29 2019 at 20:34, on Zulip):

Ah, yeah, that's quite distinct :)

Jack Huey (Oct 29 2019 at 20:35, on Zulip):

so I guess two options:

Jack Huey (Oct 29 2019 at 20:35, on Zulip):

1) return Some(Answer) with no substs and ambiguous: true

nikomatsakis (Oct 29 2019 at 20:35, on Zulip):

My main argument for panic somewhere (I'd have to go check in to the code to figure out just where) is that I would want to know if this is happening

nikomatsakis (Oct 29 2019 at 20:35, on Zulip):

and not have it get hidden

Jack Huey (Oct 29 2019 at 20:36, on Zulip):

2) Change AnswerStream to return either Result<Option<Answer>, ..>

Jack Huey (Oct 29 2019 at 20:36, on Zulip):

or I guess 3)

Jack Huey (Oct 29 2019 at 20:36, on Zulip):

panic in AnswerStream

Jack Huey (Oct 29 2019 at 20:39, on Zulip):

I think for the sake of simplicity now, I'll just panic in AnswerStream for now. If someone specifically needs to catch that outside of engine, then more edits to AnswerStream will need to be made

Jack Huey (Oct 29 2019 at 20:39, on Zulip):

Does that work?

nikomatsakis (Oct 29 2019 at 20:39, on Zulip):

Yep

Jack Huey (Oct 29 2019 at 20:50, on Zulip):

@nikomatsakis Ok I updated the PR

nikomatsakis (Oct 29 2019 at 20:51, on Zulip):

nice

Jack Huey (Oct 29 2019 at 20:51, on Zulip):

I kept the negative cycle tests but just marked them as #[should_panic]

nikomatsakis (Oct 29 2019 at 20:51, on Zulip):

perfect, thanks!

nikomatsakis (Oct 29 2019 at 20:51, on Zulip):

maybe with a comment :)

Jack Huey (Oct 29 2019 at 20:52, on Zulip):

I did add a comment in the goal block for each test

Jack Huey (Oct 29 2019 at 20:52, on Zulip):

I could add/move those to the function doc comments if you want

nikomatsakis (Oct 29 2019 at 20:56, on Zulip):

left a quick review

nikomatsakis (Oct 29 2019 at 20:57, on Zulip):

with various suggestions

Jack Huey (Oct 29 2019 at 21:00, on Zulip):

Updated :)

Jack Huey (Oct 29 2019 at 21:00, on Zulip):

Also added the panic case to the peek_answer and force_answers doc

nikomatsakis (Oct 29 2019 at 21:05, on Zulip):

nice

nikomatsakis (Oct 29 2019 at 21:08, on Zulip):

merged

Jack Huey (Oct 29 2019 at 21:09, on Zulip):

Awesome

nikomatsakis (Oct 29 2019 at 21:09, on Zulip):

I'm curious if you're interested in taking on the follow-up work around making coinduction sound :)

nikomatsakis (Oct 29 2019 at 21:10, on Zulip):

(which sort of involves re-introducing delayed literals, but in a different form)

nikomatsakis (Oct 29 2019 at 21:10, on Zulip):

https://github.com/rust-lang/chalk/issues/248

Jack Huey (Oct 29 2019 at 21:10, on Zulip):

I am curious, yes

Jack Huey (Oct 29 2019 at 21:10, on Zulip):

and interested

Jack Huey (Oct 29 2019 at 21:10, on Zulip):

I'll try to take a look at it sometime this week

Jack Huey (Oct 29 2019 at 21:12, on Zulip):

Do you have an idea of how to solve this?

Jack Huey (Oct 29 2019 at 21:12, on Zulip):

If not, it's fine. Just curious if you do

nikomatsakis (Oct 29 2019 at 22:14, on Zulip):

I do

Jack Huey (Oct 29 2019 at 22:25, on Zulip):

Would love to hear your thoughts before I start

Jack Huey (Oct 30 2019 at 02:09, on Zulip):

So while I've been sort of wrapping my head more around the cycles code, I realized that my rename from StrandFail::Cycle -> StrandFail::PositiveCycle isn't exactly accurate.

Last update: Nov 18 2019 at 01:25UTC