Merge pull request #433 from adamrk/add-more-guidance

nikomatsakis · web-flow · commit b6322c35eaf1 · 2020-05-27T18:02:33.000-04:00
Include more guidance in ambiguous results
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
@@ -136,6 +136,11 @@ pub trait ContextOps<I: Interner, C: Context<I>>:
     /// Upcast this domain goal into a more general goal.
     fn into_goal(&self, domain_goal: DomainGoal<I>) -> Goal<I>;
 
+    fn is_trivial_constrained_substitution(
+        &self,
+        constrained_subst: &Canonical<ConstrainedSubst<I>>,
+    ) -> bool;
+
     fn is_trivial_substitution(
         &self,
         u_canon: &UCanonical<InEnvironment<Goal<I>>>,
diff --git a/chalk-engine/src/forest.rs b/chalk-engine/src/forest.rs
@@ -83,7 +83,11 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
                     if !answer.ambiguous {
                         SubstitutionResult::Definite(answer.subst)
                     } else {
-                        SubstitutionResult::Ambiguous(answer.subst)
+                        if context.is_trivial_constrained_substitution(&answer.subst) {
+                            SubstitutionResult::Floundered
+                        } else {
+                            SubstitutionResult::Ambiguous(answer.subst)
+                        }
                     }
                 }
                 AnswerResult::Floundered => SubstitutionResult::Floundered,
@@ -155,7 +159,8 @@ impl<'me, I: Interner, C: Context<I>, CO: ContextOps<I, C>> AnswerStream<I>
                 .root_answer(self.context, self.table, self.answer)
             {
                 Ok(answer) => {
-                    return AnswerResult::Answer(answer.clone());
+                    debug!("Answer: {:?}", &answer);
+                    return AnswerResult::Answer(answer);
                 }
 
                 Err(RootSearchFail::InvalidAnswer) => {
diff --git a/chalk-engine/src/lib.rs b/chalk-engine/src/lib.rs
@@ -274,6 +274,12 @@ impl Minimums {
     }
 }
 
+#[derive(Copy, Clone, Debug)]
+pub(crate) enum AnswerMode {
+    Complete,
+    Ambiguous,
+}
+
 chalk_ir::copy_fold!(TableIndex);
 chalk_ir::copy_fold!(TimeStamp);
 
diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs
diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs
@@ -75,6 +75,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
                         )));
                 }
                 GoalData::CannotProve(()) => {
+                    debug!("Marking Strand as ambiguous because of a `CannotProve` subgoal");
                     ex_clause.ambiguous = true;
                 }
             }
diff --git a/chalk-engine/src/table.rs b/chalk-engine/src/table.rs
@@ -1,5 +1,5 @@
 use crate::strand::CanonicalStrand;
-use crate::Answer;
+use crate::{Answer, AnswerMode};
 use rustc_hash::FxHashMap;
 use std::collections::hash_map::Entry;
 use std::collections::VecDeque;
@@ -40,6 +40,8 @@ pub(crate) struct Table<I: Interner> {
     /// Stores the active strands that we can "pull on" to find more
     /// answers.
     strands: VecDeque<CanonicalStrand<I>>,
+
+    pub(crate) answer_mode: AnswerMode,
 }
 
 index_struct! {
@@ -60,6 +62,7 @@ impl<I: Interner> Table<I> {
             floundered: false,
             answers_hash: FxHashMap::default(),
             strands: VecDeque::new(),
+            answer_mode: AnswerMode::Complete,
         }
     }
 
@@ -80,20 +83,29 @@ impl<I: Interner> Table<I> {
         mem::replace(&mut self.strands, VecDeque::new())
     }
 
-    /// Remove the next strand from the queue as long as it meets the
-    /// given criteria.
-    pub(crate) fn dequeue_next_strand_if(
+    pub(crate) fn drain_strands(
+        &mut self,
+        test: impl Fn(&CanonicalStrand<I>) -> bool,
+    ) -> VecDeque<CanonicalStrand<I>> {
+        let old = mem::replace(&mut self.strands, VecDeque::new());
+        let (test_in, test_out): (VecDeque<CanonicalStrand<I>>, VecDeque<CanonicalStrand<I>>) =
+            old.into_iter().partition(test);
+        let _ = mem::replace(&mut self.strands, test_out);
+        test_in
+    }
+
+    /// Remove the next strand from the queue that meets the given criteria
+    pub(crate) fn dequeue_next_strand_that(
         &mut self,
         test: impl Fn(&CanonicalStrand<I>) -> bool,
     ) -> Option<CanonicalStrand<I>> {
-        let strand = self.strands.pop_front();
-        if let Some(strand) = strand {
-            if test(&strand) {
-                return Some(strand);
-            }
-            self.strands.push_front(strand);
+        let first = self.strands.iter().position(test);
+        if let Some(first) = first {
+            self.strands.rotate_left(first);
+            self.strands.pop_front()
+        } else {
+            None
         }
-        None
     }
 
     /// Mark the table as floundered -- this also discards all pre-existing answers,
diff --git a/chalk-solve/src/infer.rs b/chalk-solve/src/infer.rs
@@ -150,14 +150,6 @@ impl<I: Interner> InferenceTable<I> {
         }
     }
 
-    /// Returns true if `var` has been bound.
-    pub(crate) fn var_is_bound(&mut self, var: InferenceVar) -> bool {
-        match self.unify.probe_value(EnaVariable::from(var)) {
-            InferenceValue::Unbound(_) => false,
-            InferenceValue::Bound(_) => true,
-        }
-    }
-
     /// Given an unbound variable, returns its universe.
     ///
     /// # Panics
@@ -169,44 +161,6 @@ impl<I: Interner> InferenceTable<I> {
             InferenceValue::Bound(_) => panic!("var_universe invoked on bound variable"),
         }
     }
-
-    /// Check whether the given substitution is the identity substitution in this
-    /// inference context.
-    pub(crate) fn is_trivial_substitution(
-        &mut self,
-        interner: &I,
-        subst: &Substitution<I>,
-    ) -> bool {
-        for value in subst.as_parameters(interner) {
-            match value.data(interner) {
-                GenericArgData::Ty(ty) => {
-                    if let Some(var) = ty.inference_var(interner) {
-                        if self.var_is_bound(var) {
-                            return false;
-                        }
-                    }
-                }
-
-                GenericArgData::Lifetime(lifetime) => {
-                    if let Some(var) = lifetime.inference_var(interner) {
-                        if self.var_is_bound(var) {
-                            return false;
-                        }
-                    }
-                }
-
-                GenericArgData::Const(constant) => {
-                    if let Some(var) = constant.inference_var(interner) {
-                        if self.var_is_bound(var) {
-                            return false;
-                        }
-                    }
-                }
-            }
-        }
-
-        true
-    }
 }
 
 pub(crate) trait ParameterEnaVariableExt<I: Interner> {
diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs
@@ -423,8 +423,9 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
         // inference as an ambiguous solution.
 
         let interner = self.solver.program.interner();
+        let canonical_subst = self.infer.canonicalize(interner, &subst);
 
-        if self.infer.is_trivial_substitution(interner, &subst) {
+        if canonical_subst.quantified.value.is_identity_subst(interner) {
             // In this case, we didn't learn *anything* definitively. So now, we
             // go one last time through the positive obligations, this time
             // applying even *tentative* inference suggestions, so that we can
@@ -441,10 +442,9 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
                     } = self.prove(&goal, minimums).unwrap();
                     if let Some(constrained_subst) = solution.constrained_subst() {
                         self.apply_solution(free_vars, universes, constrained_subst);
-                        let subst = self
-                            .infer
-                            .canonicalize(self.solver.program.interner(), &subst);
-                        return Ok(Solution::Ambig(Guidance::Suggested(subst.quantified)));
+                        return Ok(Solution::Ambig(Guidance::Suggested(
+                            canonical_subst.quantified,
+                        )));
                     }
                 }
             }
@@ -471,10 +471,9 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
             // for sure what `T` must be (it could be either `Foo<Bar>` or
             // `Foo<Baz>`, but we *can* say for sure that it must be of the
             // form `Foo<?0>`.
-            let subst = self
-                .infer
-                .canonicalize(self.solver.program.interner(), &subst);
-            Ok(Solution::Ambig(Guidance::Definite(subst.quantified)))
+            Ok(Solution::Ambig(Guidance::Definite(
+                canonical_subst.quantified,
+            )))
         }
     }
 
diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs
@@ -190,6 +190,14 @@ impl<'me, I: Interner> context::ContextOps<I, SlgContext<I>> for SlgContextOps<'
         domain_goal.cast(self.program.interner())
     }
 
+    fn is_trivial_constrained_substitution(
+        &self,
+        constrained_subst: &Canonical<ConstrainedSubst<I>>,
+    ) -> bool {
+        let interner = self.interner();
+        constrained_subst.value.subst.is_identity_subst(interner)
+    }
+
     fn is_trivial_substitution(
         &self,
         u_canon: &UCanonical<InEnvironment<Goal<I>>>,
diff --git a/chalk-solve/src/solve/slg/aggregate.rs b/chalk-solve/src/solve/slg/aggregate.rs
@@ -40,9 +40,13 @@ impl<I: Interner> context::AggregateOps<I, SlgContext<I>> for SlgContextOps<'_,
         // Exactly 1 unconditional answer?
         let next_answer = answers.peek_answer(|| should_continue());
         if next_answer.is_quantum_exceeded() {
-            return Some(Solution::Ambig(Guidance::Suggested(
-                subst.map(interner, |cs| cs.subst),
-            )));
+            if subst.value.subst.is_identity_subst(interner) {
+                return Some(Solution::Ambig(Guidance::Unknown));
+            } else {
+                return Some(Solution::Ambig(Guidance::Suggested(
+                    subst.map(interner, |cs| cs.subst),
+                )));
+            }
         }
         if next_answer.is_no_more_solutions() && !ambiguous {
             return Some(Solution::Unique(subst));
diff --git a/tests/test/impls.rs b/tests/test/impls.rs
@@ -639,3 +639,41 @@ fn clauses_in_if_goals() {
         }
     }
 }
+
+#[test]
+fn unify_types_in_ambiguous_impl() {
+    test! {
+        program {
+            #[non_enumerable]
+            trait Constraint {}
+            trait Trait<T> {}
+            struct A<T> {}
+            impl<T> Trait<T> for A<T> where T: Constraint {}
+        }
+
+        goal {
+            exists<T,U> { A<T>: Trait<U> }
+        } yields {
+            "Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := ^0.0] }"
+        }
+    }
+}
+
+#[test]
+fn unify_types_in_impl() {
+    test! {
+        program {
+            #[non_enumerable]
+            trait Constraint {}
+            trait Trait<T> {}
+            struct A<T> {}
+            impl<T> Trait<T> for A<T> {}
+        }
+
+        goal {
+            exists<T,U> { A<T>: Trait<U> }
+        } yields {
+            "Unique; for<?U0> { substitution [?0 := ^0.0, ?1 := ^0.0], lifetime constraints [] }"
+        }
+    }
+}
diff --git a/tests/test/misc.rs b/tests/test/misc.rs
@@ -176,10 +176,11 @@ fn subgoal_cycle_uninhabited() {
         }
 
         // Infinite recursion -> we flounder
+        // Still return the necessary substitution T = Box<..>
         goal {
             exists<T> { T: Foo }
         } yields_first[SolverChoice::slg(2, None)] {
-            "Floundered"
+            "Ambiguous(for<?U0> { substitution [?0 := Box<^0.0>], lifetime constraints [] })"
         }
 
         // Unsurprisingly, applying negation also flounders.
@@ -201,7 +202,7 @@ fn subgoal_cycle_uninhabited() {
         goal {
             exists<T> { T = Vec<Alice>, not { Vec<Vec<T>>: Foo } }
         } yields_first[SolverChoice::slg(2, None)] {
-            "Floundered"
+            "Ambiguous(substitution [?0 := Vec<Alice>], lifetime constraints [])"
         }
 
         // Same query with larger threshold works fine, though.
@@ -216,7 +217,7 @@ fn subgoal_cycle_uninhabited() {
             forall<U> { if (U: Foo) { exists<T> { T: Foo } } }
         } yields_first[SolverChoice::slg(2, None)] {
             "substitution [?0 := !1_0], lifetime constraints []",
-            "Floundered"
+            "Ambiguous(for<?U1> { substitution [?0 := Box<^0.0>], lifetime constraints [] })"
         }
     }
 }
@@ -234,11 +235,12 @@ fn subgoal_cycle_inhabited() {
         }
 
         // Exceeds size threshold -> flounder
+        // Still return necessary substitution T = Box<..>
         goal {
             exists<T> { T: Foo }
         } yields_first[SolverChoice::slg(3, None)] {
             "substitution [?0 := Alice], lifetime constraints []",
-            "Floundered"
+            "Ambiguous(for<?U0> { substitution [?0 := Box<^0.0>], lifetime constraints [] })"
         }
     }
 }
@@ -555,3 +557,58 @@ fn builtin_impl_enumeration() {
         }
     }
 }
+
+/// Don't return definite guidance if we flounder after finding one solution.
+#[test]
+fn flounder_ambiguous() {
+    test! {
+        program {
+            trait IntoIterator { }
+            #[non_enumerable]
+            trait OtherTrait { }
+
+            struct Ref<T> { }
+            struct A { }
+
+            impl IntoIterator for Ref<A> { }
+            impl<T> IntoIterator for Ref<T> where T: OtherTrait { }
+        }
+
+        goal {
+            exists<T> { Ref<T>: IntoIterator }
+        } yields {
+            "Ambiguous; no inference guidance"
+        }
+    }
+}
+
+/// 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"
+        }
+    }
+}
diff --git a/tests/test/projection.rs b/tests/test/projection.rs

Original file line number	Diff line number	Diff line change
`@@ -83,7 +83,11 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {`
`83`	`83`	`if !answer.ambiguous {`
`84`	`84`	`SubstitutionResult::Definite(answer.subst)`
`85`	`85`	`} else {`
`86`		`- SubstitutionResult::Ambiguous(answer.subst)`
	`86`	`+ if context.is_trivial_constrained_substitution(&answer.subst) {`
	`87`	`+ SubstitutionResult::Floundered`
	`88`	`+ } else {`
	`89`	`+ SubstitutionResult::Ambiguous(answer.subst)`
	`90`	`+ }`
`87`	`91`	`}`
`88`	`92`	`}`
`89`	`93`	`AnswerResult::Floundered => SubstitutionResult::Floundered,`
`@@ -155,7 +159,8 @@ impl<'me, I: Interner, C: Context<I>, CO: ContextOps<I, C>> AnswerStream<I>`
`155`	`159`	`.root_answer(self.context, self.table, self.answer)`
`156`	`160`	`{`
`157`	`161`	`Ok(answer) => {`
`158`		`- return AnswerResult::Answer(answer.clone());`
	`162`	`+ debug!("Answer: {:?}", &answer);`
	`163`	`+ return AnswerResult::Answer(answer);`
`159`	`164`	`}`
`160`	`165`
`161`	`166`	`Err(RootSearchFail::InvalidAnswer) => {`
Original file line number	Diff line number	Diff line change
`@@ -274,6 +274,12 @@ impl Minimums {`
`274`	`274`	`}`
`275`	`275`	`}`
`276`	`276`
	`277`	`+#[derive(Copy, Clone, Debug)]`
	`278`	`+pub(crate) enum AnswerMode {`
	`279`	`+ Complete,`
	`280`	`+ Ambiguous,`
	`281`	`+}`
	`282`	`+`
`277`	`283`	`chalk_ir::copy_fold!(TableIndex);`
`278`	`284`	`chalk_ir::copy_fold!(TimeStamp);`
`279`	`285`
Original file line number	Diff line number	Diff line change
`@@ -75,6 +75,7 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {`
`75`	`75`	`)));`
`76`	`76`	`}`
`77`	`77`	`GoalData::CannotProve(()) => {`
	`78`	+ debug!("Marking Strand as ambiguous because of a `CannotProve` subgoal");
`78`	`79`	`ex_clause.ambiguous = true;`
`79`	`80`	`}`
`80`	`81`	`}`