Include more guidance in ambiguous results

[adamrk]

There are situations where chalk a query is ambiguous and chalk returns Ambig(Guidance::Unknown) even though it has deduced some non-trivial substitutions. For example, with this program:

#[non_enumerable]
trait Constraint {}
trait Trait<T> {}
struct A<T> {}
impl<T> Trait<T> for A<T> where T: Constraint {}

the query exists<T,U> { A<T>: Trait<U> } flounders because we can't determine if there is a solution to T: Constraint and the result is Ambig(Guidance::Unknown). But even with an ambiguous result we should still be able to return the guidance that T = U.

The ambiguous guidance in situations like this will be useful in rust-analyzer where some queries flounder because all traits are treated as non_enumerable (see e.g. rust-lang/rust-analyzer#4072).

The changes here check if any substitutions have been deduced when a goal flounders and returning an ambiguous guidance if the substitutions deduced so far are non-trivial.

Closes #331
Closes #429

[adamrk]

Made some changes that seem to work for the slg solver, but I still need to clean it up into something presentable.

[flodiebold]

The recursive solver part LGTM, for the SLG part @jackh726 or @nikomatsakis would need to take a look. You wrote you still wanted to clean it up, is that still the case or is this ready for review?

[jackh726]

Nice :)

Some comments, but overall I think I like the approach

[jackh726]

I'm also curious if this has any effect on the issue here: #331

[jackh726]

Okay, so after looking around a bit, I think I'm convinced that this isn't quite correct on the SLG side. Particularly, I think that adding answers when there are still floundered subgoals is not possible to do correctly yet. This seems to work if you don't push an ambiguous trivial substitution. But I think that's because we don't have any test cases that have a non-ambiguous non-trivial substitution for a strand with all floundered subgoals and will eventually get solved later.

[jackh726]

I'm not quite sure the best way to approach this though. Part of me wonders if, instead of adding incomplete (meaning there are still floundered subgoals) answers always, we instead only do this if we can no longer make progress anywhere. I think we can do this by essentially doing two passes for subgoals: once where subgoals can't create ambiguous or incomplete answers, then a second where they can. (I wonder if it's even worth splitting this into three: one "complete and umabiguous", one "complete and ambiguous", and one "incomplete and ambiguous"). I guess I have to think if we have to do this globally or if per-Strand is enough. (i.e. if another Strand is followed, will subgoals of the current Strand ever become non-ambiguous. I think the answer is no, but have to look.)

Edit: right, we only reconsider floundered subgoals if there are new answers to the current Strand

[jackh726]

I have a partial fix for this locally. It fixed iterator_flatten, but not non_enumerable_traits_reorder yet

[jackh726]

Okay I completed the fix. (You can see them here: master...jackh726:add-more-guidance)

I essentially split answer generation into "complete" and "ambiguous" phases. Basically, we always be sure to process non-ambiguous answers first. For the purposes of answers, any answer we get from strands with all floundered subgoals is ambiguous (which like in this PR we actually use).

In general, it needs a bit more cleaning up before it can be used/merged. A couple things to start:

• general cleanup
• I think on_subgoal_selection_flounder is never called. Or at least, it doesn't really make sense anymore
• (Not really from this PR, but I came across this) I think we can remove the call to merge_answer_into_strand in on_no_remaining_subgoals and just let the loop merge in the tabled answer in on_subgoal_selected (the same strand will stay active)
• We should never be hitting the "New answer was not ambiguous whereas previous answer was." panic now. Need to think about this.
• I think we should be merging in all the the floundered subgoals into the subst in pursue_answer

It might be worth splitting my changes out into a separate PR before this since it's kind of a lot on it's own, but also technically an independent fix.

[adamrk]

Cool, thanks! Either way sounds good to me. I could start working on some of the cleanup of your branch?

[jackh726]

@adamrk I think I can finish the cleanup pretty soon. Did you enable the option for me to be able to push to your branch?

Also, these changes fix the tests in #331. Which is fantastic because this highlights that the changes here are a little bit more fundamental to how we handle ambiguous answers than just including more guidance :)

[adamrk]

Sounds good! Yeah I turned on edits by maintainers.

[jackh726]

Okay, done with cleanups.

@nikomatsakis care to take a look at this? A quick summary/tldr of this thread and PR:
In chalk-engine, we now always generate an answer for a strand, even if there are floundered subgoals. To correctly handle this, we split solving a goal into two stages (AnswerMode) either Complete, where we don't allow ambiguous answers (answers from strands with floundered subgoals count as ambiguous), and Ambiguous where we do allow ambiguous answers.

This was basically done to fix this case:

chalk/chalk-engine/src/table.rs

Line 138 in 80c17b8

panic!("New answer was not ambiguous whereas previous answer was.");

. We've talked about this previously, but never had a test that actually hit this. Unfortunately, I don't think there's a better way to actually allow ambiguous answers before non-ambiguous answers.

This also has the side-effect of fixing some other tests as well, including those from #331 and #429, so these changes definitely are a bit more fundamental to how we handle ambiguous answers than just giving some extra guidance.