Don't return definite guidance if we find one solution and then flounder #331

flodiebold · 2020-02-15T15:37:01Z

If we find one solution and then flounder, this previously resulted in a Guidance::Definite result. I think the reason is that any_future_answer has no answers to check and hence returns true.

This adds some tools helpful when debugging nondeterminism in analysis-stats: - a `--randomize` option that analyses everything in random order - a `-vv` option that prints even more detail Also add a debug log if Chalk fuel is exhausted (which would be a source of nondeterminism, but didn't happen in my tests). I found one source of nondeterminism (rust-lang/chalk#331), but there are still other cases remaining.

flodiebold · 2020-02-15T17:09:33Z

I think there may still be a problem with the any_future_answer check, because I found another case where we sometimes erroneously get definite guidance; in that case, there's more than one solution, but the first few solutions are all of the form &?0, so we get back &?0 as guidance. I'm not seeing any floundering in that case.

3157: Extend analysis-stats a bit r=matklad a=flodiebold This adds some tools helpful when debugging nondeterminism in analysis-stats: - a `--randomize` option that analyses everything in random order - a `-vv` option that prints even more detail Also add a debug log if Chalk fuel is exhausted (which would be a source of nondeterminism, but didn't happen in my tests). I found one source of nondeterminism (rust-lang/chalk#331), but there are still other cases remaining. Co-authored-by: Florian Diebold <flodiebold@gmail.com>

jackh726 · 2020-02-15T23:25:15Z

I have to think about this a bit more, but I don't think this fix is the most correct one to make.

I think the reason is that any_future_answer has no answers to check and hence returns true.
Well, that can't be the case because it can still Flounder.

This might be a problem with MayInvalidate, but I don't know yet.

Nevertheless, thanks for the test. If you remove non_enumerable from OtherTrait, it returns Ambiguous right? Also, can you add a short comment to the test to explain what it is for? Thanks.

flodiebold · 2020-02-16T10:00:42Z

I have to think about this a bit more, but I don't think this fix is the most correct one to make.

That's very possible, especially since there still seems to be some similar problem.

Nevertheless, thanks for the test. If you remove non_enumerable from OtherTrait, it returns Ambiguous right?

Yes.

Also, can you add a short comment to the test to explain what it is for? Thanks.

Done.

flodiebold · 2020-02-16T16:45:45Z

Ok, I was able to reproduce the second problem:

/// Don't return definite guidance if we are able to merge two solutions and the
/// third one matches that as well (the fourth may not).
#[test]
fn normalize_ambiguous() {
    test! {
        program {
            trait IntoIterator { type Item; }

            struct Ref<T> { }
            struct A { }
            struct B { }
            struct C { }

            struct D { }

            impl IntoIterator for Ref<A> { type Item = Ref<A>; }
            impl IntoIterator for Ref<B> { type Item = Ref<B>; }
            impl IntoIterator for Ref<C> { type Item = Ref<C>; }
            impl IntoIterator for Ref<D> { type Item = D; }
        }

        goal {
            exists<T, U> {
                Normalize(<Ref<T> as IntoIterator>::Item -> U)
            }
        } yields {
            "Ambiguous; no inference guidance"
        }
    }
}

This currently results in

Ambiguous; definite substitution for<?U0,?U0> { [?0 := ^0, ?1 := Ref<^1>] }

because any_future_answer actually just looks at the next answer, which happens to match in this case.

jackh726 · 2020-02-17T03:02:59Z

any_future_answer will test every strand with MayInvalidate. So this again points to MayInvalidate not being correct.

jackh726 · 2020-02-17T03:13:04Z

Also, this test (in the comment) passes on current master, but not with the changes in this PR.

flodiebold · 2020-02-17T07:59:04Z

Also, this test (in the comment) passes on current master, but not with the changes in this PR.

Ah, I think with my change it hits the 'answer cached' case:

chalk/chalk-engine/src/logic.rs

Lines 213 to 216 in f85bb2e

    
           if let Some(answer) = self.tables[table].answer(answer) { 
        
               info!("answer cached = {:?}", answer); 
        
               return test(C::inference_normalized_subst_from_subst(&answer.subst)); 
        
           }

nikomatsakis · 2020-03-03T10:29:12Z

chalk-solve/src/solve/slg/aggregate.rs

@@ -69,6 +69,10 @@ impl<I: Interner> context::AggregateOps<SlgContext<I>> for SlgContextOps<'_, I>
                break Guidance::Unknown;
            }

+            if let AnswerResult::Floundered = answers.peek_answer(|| should_continue()) {
+                break Guidance::Suggested(subst);


Hmm, I think if we floundered we probably want Guidance::Unknown, as that suggests that we never really explored the options.

nikomatsakis · 2020-03-03T10:31:01Z

But I see there were a lot more comments :) I have to read those and fully grok what they're saying

This adds some tools helpful when debugging nondeterminism in analysis-stats: - a `--randomize` option that analyses everything in random order - a `-vv` option that prints even more detail Also add a debug log if Chalk fuel is exhausted (which would be a source of nondeterminism, but didn't happen in my tests). I found one source of nondeterminism (rust-lang/chalk#331), but there are still other cases remaining.

nikomatsakis

@flodiebold would you be up to rebase this, but return Guidance::Unknown in the case of floundering?

If we find one solution and then flounder, this previously resulted in a `Guidance::Definite` result. I think the reason is that `any_future_answer` has no answers to check and hence returns true.

flodiebold · 2020-04-14T21:15:24Z

@nikomatsakis Done! I added the second test as well, with the currently wrong result.

nikomatsakis · 2020-04-15T13:24:06Z

tests/test/misc.rs

+/// Don't return definite guidance if we are able to merge two solutions and the
+/// third one matches that as well (the fourth may not).
+#[test]
+fn normalize_ambiguous() {


Does this test have anything to do with floundering?

I don't think so (except that this test only reproduces the problem with the fix for the other problem, I think because it calls peek_answer)

I see, curious.

nikomatsakis · 2020-04-15T13:24:16Z

tests/test/misc.rs

+                Normalize(<Ref<T> as IntoIterator>::Item -> U)
+            }
+        } yields {
+            // FIXME: this is wrong!


We should probably create a FIXME policy of creating open issues to track these...

nikomatsakis · 2020-04-17T10:37:52Z

I'm confused I guess if we want to land this now and investigate later or do more investigation. It seems like it's improving some problems you encountered in rust-analyzer?

flodiebold · 2020-04-17T10:55:11Z

I think we could land this now. It's not that important for rust-analyzer anymore though since I switched to the recursive solver ;)

flodiebold mentioned this pull request Feb 15, 2020

Extend analysis-stats a bit rust-lang/rust-analyzer#3157

Merged

flodiebold force-pushed the flounder-ambiguous branch from def4cf4 to f1ce23a Compare February 16, 2020 10:00

nikomatsakis requested changes Mar 3, 2020

View reviewed changes

nikomatsakis requested changes Apr 14, 2020

View reviewed changes

Don't return definite guidance if we find one solution and then flounder

9d655f4

If we find one solution and then flounder, this previously resulted in a `Guidance::Definite` result. I think the reason is that `any_future_answer` has no answers to check and hence returns true.

flodiebold force-pushed the flounder-ambiguous branch from f1ce23a to 9d655f4 Compare April 14, 2020 21:14

nikomatsakis reviewed Apr 15, 2020

View reviewed changes

jackh726 mentioned this pull request May 21, 2020

Include more guidance in ambiguous results #433

Merged

jackh726 added a commit to jackh726/chalk that referenced this pull request May 25, 2020

Add regression tests from PR rust-lang#331

c9a67ae

nikomatsakis closed this in #433 May 27, 2020

nathanwhit pushed a commit to nathanwhit/chalk that referenced this pull request May 28, 2020

Add regression tests from PR rust-lang#331

8c026f4

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Don't return definite guidance if we find one solution and then flounder #331

Don't return definite guidance if we find one solution and then flounder #331

flodiebold commented Feb 15, 2020

flodiebold commented Feb 15, 2020 •

edited

Loading

jackh726 commented Feb 15, 2020

flodiebold commented Feb 16, 2020

flodiebold commented Feb 16, 2020

jackh726 commented Feb 17, 2020

jackh726 commented Feb 17, 2020 •

edited

Loading

flodiebold commented Feb 17, 2020

nikomatsakis Mar 3, 2020

nikomatsakis commented Mar 3, 2020

nikomatsakis left a comment

flodiebold commented Apr 14, 2020

nikomatsakis Apr 15, 2020

flodiebold Apr 15, 2020

nikomatsakis Apr 15, 2020

nikomatsakis Apr 15, 2020

nikomatsakis commented Apr 17, 2020

flodiebold commented Apr 17, 2020

Don't return definite guidance if we find one solution and then flounder #331

Don't return definite guidance if we find one solution and then flounder #331

Conversation

flodiebold commented Feb 15, 2020

flodiebold commented Feb 15, 2020 • edited Loading

jackh726 commented Feb 15, 2020

flodiebold commented Feb 16, 2020

flodiebold commented Feb 16, 2020

jackh726 commented Feb 17, 2020

jackh726 commented Feb 17, 2020 • edited Loading

flodiebold commented Feb 17, 2020

nikomatsakis Mar 3, 2020

Choose a reason for hiding this comment

nikomatsakis commented Mar 3, 2020

nikomatsakis left a comment

Choose a reason for hiding this comment

flodiebold commented Apr 14, 2020

nikomatsakis Apr 15, 2020

Choose a reason for hiding this comment

flodiebold Apr 15, 2020

Choose a reason for hiding this comment

nikomatsakis Apr 15, 2020

Choose a reason for hiding this comment

nikomatsakis Apr 15, 2020

Choose a reason for hiding this comment

nikomatsakis commented Apr 17, 2020

flodiebold commented Apr 17, 2020

flodiebold commented Feb 15, 2020 •

edited

Loading

jackh726 commented Feb 17, 2020 •

edited

Loading