Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix coinductive unsoundness #272

Merged
merged 6 commits into from Dec 23, 2019
Merged

Fix coinductive unsoundness #272

merged 6 commits into from Dec 23, 2019

Conversation

@jackh726
Copy link
Contributor

jackh726 commented Oct 30, 2019

Fixes #248

Now, when a coinductive cycle is found, it is marked in PositiveCycle as such. In pursue_strand, these are ignored until all other subgoals have been proven. Once that is the case, we can assume that the coinductive cycles are true.

With this, I also did a lot of refactoring in terms of how the recursion is handled. Importantly, I moved the calls ensure_answer_recursively and pursue_strand_recursively out of pursue_positive_subgoal and pursue_negative_subgoal, which ends up making it really obvious that purse_strand can easily be done using a loop instead of recursion. So now, the stack protection feature is no longer needed.

chalk-engine/src/logic.rs Outdated Show resolved Hide resolved
@nikomatsakis nikomatsakis self-assigned this Nov 1, 2019
Copy link
Collaborator

nikomatsakis left a comment

first round of comments -- I'm still trying to work through the "mildly nervous" comment to decide if I see an actual problem :)

chalk-engine/src/logic.rs Outdated Show resolved Hide resolved
chalk-engine/src/logic.rs Outdated Show resolved Hide resolved
chalk-engine/src/logic.rs Outdated Show resolved Hide resolved
chalk-engine/src/logic.rs Outdated Show resolved Hide resolved
chalk-engine/src/logic.rs Outdated Show resolved Hide resolved
.ex_clause
.subgoals
.extend(strand.ex_clause.delayed_coinductive_cycles.drain(..));
allow_coinduction = true;

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Nov 4, 2019

Collaborator

I'm mildly nervous about this and I'm trying to figure out why. I think my concern is something like this:

  • we encounter a co-inductive cycle and put it aside
  • we solve all remaining goals
  • then as part of processing that coinductive subgoal, we generate a new subgoal

This comment has been minimized.

Copy link
@jackh726

jackh726 Nov 4, 2019

Author Contributor

Hmm, I have to think about if that is possible. I don't think so, because the PositiveCycle is returned before any chance to make a new subgoal is reached.

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Nov 4, 2019

Collaborator

I also suspect not, but I wanted to trace out the flow and convince myself. :)

This comment has been minimized.

Copy link
@jackh726

jackh726 Nov 5, 2019

Author Contributor

FWIW, I'll add a comment to make sure this assertion explicit. (And also go through and verify).

This comment has been minimized.

Copy link
@jackh726

jackh726 Nov 5, 2019

Author Contributor

I also don't know what it would mean to add subgoals to a strand? Sure, we move subgoals to floundering and to delayed_coinductive, but they aren't "created" really after the initial simplify_hh_goal. Otherwise, if new subgoals can be added at any time, then that makes keeping track of whether or not a strand is "complete" much more difficult.

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Nov 5, 2019

Collaborator

They can in fact be created by every unification. This is partly what I've been attempting to refactor away, but I don't think we're going to be able to do that completely.

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Nov 5, 2019

Collaborator

Although I realize now that we actually could

@jackh726 jackh726 force-pushed the jackh726:coinductive branch from b769764 to c10357c Nov 5, 2019
Copy link
Collaborator

nikomatsakis left a comment

(dummy review, ignore)

@jackh726

This comment has been minimized.

Copy link
Contributor Author

jackh726 commented Nov 5, 2019

I did make a new test that should work but instead panics. So this PR isn't ready.

#[test]
fn coinductive_multicycle() {
    test! {
        program {
            trait Any { }

            #[auto]
            trait C1 { }

            #[auto]
            trait C2 { }

            #[auto]
            trait C3 { }

            trait C4 { }

            forall<T> {
                T: C1 if T: C2
            }

            forall<T> {
                T: C2 if T: C3
            }

            forall<T> {
                T: C3 if T: C1
            }

            forall<T> {
                T: Any if T: C3
            }

            forall<T> {
                T: Any if T: C2
            }

            forall<T> {
                T: Any if T: C1
            }
        }

        goal {
            forall<X> { X: Any }
        } first 10 with max 3 {
            r"[]"
        }
    }
}
@jackh726

This comment has been minimized.

Copy link
Contributor Author

jackh726 commented Nov 6, 2019

@nikomatsakis Ok I've updated so that the test (and a couple more) pass.

To summarize the updated changes: A strand is marked as EnsureSuccess::Coinductive if all remaining subgoals are coinductive (either by propogation up the stack, or from a direct cycle). Only when a Coinductive success reaches the root can it be turned into an answer. This means that all strands on the stack only had coinductive subgoals.

@jackh726 jackh726 force-pushed the jackh726:coinductive branch from 2e9f854 to 19271f8 Nov 6, 2019
@nikomatsakis

This comment has been minimized.

Copy link
Collaborator

nikomatsakis commented Nov 6, 2019

@jackh726 I'll take a look. I had these two "inklings" I was pursuing with the old branch to try and turn into failing test cases. I can't quite tell if your test matches them.

Suspicion 1. The old code at least just checked whether something was coinductive, but it didn't look at how far up the stack the "coinduction" went. This seemed problematic. I suspect your recent changes address this.

Suspicion 2. When things recurse, it means that they match the same goal, but those goals can have unknown variables. I worry that we might have a recursion that only works for some values of those variables and it might not get detected.

@nikomatsakis

This comment has been minimized.

Copy link
Collaborator

nikomatsakis commented Nov 8, 2019

OK, I read through the latest version. Let me see if I can summarize what happens:

  • When a (coinductive) cycle is encountered, the subgoal is recorded in the strand.
  • This strand does not record a regular answer, but instead returns a CoinductiveSuccess with itself (canonicalized).
  • If this is not the top of the stack, that strand will be stored back into its table by the caller. The caller will then mark its own goal as coinductive and keep going.
  • If it is the root strand, and once all other subgoals are completed, we will consider it to be an answer.

I think this is going in the right direction but I have a few concerns:

First, I don't think it's correct to special case the root strand. We should be leveraging the depth here. In other words, the root of the coinductive cycle may not be the root of the overall stack.

Second, I think it would be better if the reasoning regarding strands was more local -- this logic feels very spread out to me and kind of harder to follow.

I left some notes on how I had imagined it working but I think I still need to try to make that more concrete. I will try to do this later today if I get a chance.

One thing I was wondering was whether there are smaller refactorings that we can pull out from this PR?

@jackh726 jackh726 force-pushed the jackh726:coinductive branch 9 times, most recently from ce90b13 to b6c2d4d Nov 8, 2019
chalk-engine/src/logic.rs Outdated Show resolved Hide resolved
let table_goal = &self.tables[table].table_goal;
dbg!(&delayed_subgoal);
dbg!(&table_goal);
if delayed_subgoal == *table_goal {

This comment has been minimized.

Copy link
@jackh726

jackh726 Nov 11, 2019

Author Contributor

Right now, I'm only checking for equality. This is obviously not sufficient (see cyclic_wf_requirements test). What's the best way to do this?

This comment has been minimized.

Copy link
@jackh726

jackh726 Nov 13, 2019

Author Contributor

This has been moved to goals_trivially_equal but the same comment applies.

@@ -442,6 +442,24 @@ where
}
}

impl<T, TF> Fold<TF> for UCanonical<T>

This comment has been minimized.

Copy link
@jackh726

jackh726 Nov 11, 2019

Author Contributor

I'm honestly not 100% sure what Fold does (or why). Does this make sense?

chalk-engine/src/logic.rs Outdated Show resolved Hide resolved
@jackh726

This comment has been minimized.

Copy link
Contributor Author

jackh726 commented Nov 12, 2019

Ok so I spent a bit of time digging into why two of the tests I added (coinductive_conflicting2 and coinductive_conflicting3) are failing.

So, basically the C1 and C2 tables are Floundering because of the first check in program_clauses in chalk-solve/solve/slg. I still need to think about the logic here. But it seems separate from the coinductive cycles.

@jackh726

This comment has been minimized.

Copy link
Contributor Author

jackh726 commented Nov 21, 2019

Before this is merged, it will definitely need to rebased to master. Additionally, there are some design questions I'm unsure about that need review and a second pair of eyes. Some are marked by FIXMEs in the code. Additionally:

  • I'm not sure if the way I'm applying the binders to the delayed subgoals is correct. It works for all the current and new tests, but I'm not sure if it's correct for all cases. If there are cases where it might not work, tests should be added. I tried to add a couple tests that I thought would break it, but it works as expected.
  • Need to think about when a delayed subgoal can/would Flounder.
  • In what cases will a delayed subgoal have a substitution and how does this get applied.
  • The refinement part of this actually will probably be easier after #281 is merged.
@nikomatsakis

This comment has been minimized.

Copy link
Collaborator

nikomatsakis commented Dec 7, 2019

@jackh726 will you be able to rebase this atop the new master, which includes the nonrecursive changes?

@jackh726

This comment has been minimized.

Copy link
Contributor Author

jackh726 commented Dec 7, 2019

@nikomatsakis yes I'll do it this weekend

@jackh726 jackh726 force-pushed the jackh726:coinductive branch 3 times, most recently from 0904da0 to e850d83 Dec 7, 2019
@jackh726 jackh726 force-pushed the jackh726:coinductive branch from e850d83 to d7ceefa Dec 7, 2019
@jackh726

This comment has been minimized.

Copy link
Contributor Author

jackh726 commented Dec 7, 2019

@nikomatsakis This has been rebased to master

@jackh726 jackh726 force-pushed the jackh726:coinductive branch from d7ceefa to c15ba79 Dec 7, 2019
@jackh726 jackh726 force-pushed the jackh726:coinductive branch 2 times, most recently from 08275ef to 2366036 Dec 16, 2019
Copy link
Collaborator

nikomatsakis left a comment

Yes, this last commit looks like what I had in mind -- apart from a nit about the comment, @jackh726, I think this may be ready to land? Are there further changes you have planned (at least, changes that should land in this PR?)

@@ -679,16 +678,29 @@ impl<C: Context> Forest<C> {
let (table, subst, constraints, delayed_subgoals) =
context.instantiate_answer_subst(num_universes, &answer.subst);

// FIXME: really, these shouldn't be added to the delayed_subgoals at all
// however, because we can't compare the table goal until `canonicalize_answer_subst`
// is called in `pursue_answer`, this will require a bit of refactoring work

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Dec 21, 2019

Collaborator

I don't really understand this comment -- oh, are you saying that "really there shouldn't be anything in delayed_subgoals that is equal to table_goal? If so, I'm not sure I agree, I think that can arise after unification, but you are correct that detecting that equality cannot reliably be done with ==. (But you don't need unification, we could make a method that does it.) Anyway, if that's what you mean, I agree, but we should probably file an issue and/or write a better comment.

This comment has been minimized.

Copy link
@jackh726

jackh726 Dec 21, 2019

Author Contributor

Ok, so there's a couple things going on here, and I'll try to explain it succinctly since I'm traveling today (so on mobile at least for the minute).

So first, it's maybe not obvious from the PR (and maybe not even wrong), but something I found when looking through CHALK_DEBUG output. But in apply_answer_subst, we can't properly check if the delayed subgoals are equal to the table goal, because the delayed subgoals get unique inference variables. (Perhaps this would be easier/quicker to check using the variant3 test and adding dbg statements there.)

Second, I would REALLY prefer to have these be checked before they are added to the answer. But, because of 1, we have to wait until they are both canonicalized, which happens in pursue_answer. At that point it is too late because that doesn't know about the subgoal. That was mostly the point of this FIXME: we can be smarter here I think, but it requires a bit of refactoring.

Third, there are essentially two places that do this check. First is in apply_answer_subst and second is here. They aren't the same: removing this causes the variant3 test to fail. Removing the other causes...many of the conductive tests to fail (and a never-ending test for one that I don't remember off the top of my head). I'm not convinced that there couldn't be just one check in the right place.

So, overall. I'm a bit skeptical. Between both checks, everything works. But as I said, I don't know if it's perfectly correct and I definitely think there's room for improvement. Whether that needs to be done in this PR or can be done separately idk.

Nonetheless, I should have some time soon to, at the very least, cleanup this FIXME and a couple other things. (Like the extra apply_binders function that was added but isn't used anymore). If we decide to land the PR as is, I'll file a followup issue with more detailed info.

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Dec 22, 2019

Collaborator

OK, thanks for elaborating. Personally I'm inclined to convert this comment into an issue and land the PR, since I think it's clearly 'progress', but I definitely agree we can refactor this part of it. I'd be happy to take some time to chat it out.

@jackh726

This comment has been minimized.

Copy link
Contributor Author

jackh726 commented Dec 22, 2019

This PR is good to merge now! I'll file a followup issue for the changes we talked about, and we can discuss.

jackh726 and others added 6 commits Dec 7, 2019
…s just tells the answerstream to skip it.) For now, filter delayed subgoals that match the table goal before adding to subgoals. Really, they should be filtered before getting added to the ex-clause, but the subgoals are getting unique inference variables, so they aren't equal to the table goal. Instead, we need to filter them after canonicalization.
@nikomatsakis nikomatsakis force-pushed the jackh726:coinductive branch from ed9f81d to 6e68a41 Dec 23, 2019
@nikomatsakis

This comment has been minimized.

Copy link
Collaborator

nikomatsakis commented Dec 23, 2019

FYI @jackh726 I rebased this

@nikomatsakis nikomatsakis merged commit 44106c0 into rust-lang:master Dec 23, 2019
3 checks passed
3 checks passed
Test (stable)
Details
Test (nightly)
Details
Format
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.