include guidance for floundered goals

Author: adamrk

chalk-engine/src/context.rs

@@ -251,6 +251,11 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
     /// Upcast this domain goal into a more general goal.
     fn into_goal(&self, domain_goal: C::DomainGoal) -> C::Goal;
 
+    fn is_trivial_constrained_substitution(
+        &self,
+        constrained_subst: &C::CanonicalConstrainedSubst,
+    ) -> bool;
+
     fn is_trivial_substitution(
         &self,
         u_canon: &C::UCanonicalGoalInEnvironment,

chalk-engine/src/forest.rs

@@ -89,7 +89,12 @@ impl<C: Context> Forest<C> {
                     if !answer.ambiguous {
                         SubstitutionResult::Definite(context.constrained_subst_from_answer(answer))
                     } else {
-                        SubstitutionResult::Ambiguous(context.constrained_subst_from_answer(answer))
+                        let subst = context.constrained_subst_from_answer(answer);
+                        if context.is_trivial_constrained_substitution(&subst) {
+                            SubstitutionResult::Floundered
+                        } else {
+                            SubstitutionResult::Ambiguous(subst)
+                        }
                     }
                 }
                 AnswerResult::Floundered => SubstitutionResult::Floundered,

chalk-engine/src/logic.rs

@@ -41,6 +41,7 @@ pub(super) enum RootSearchFail {
 }
 
 /// This is returned when we try to select a subgoal for a strand.
+#[derive(PartialEq)]
 enum SubGoalSelection {
     /// A subgoal was successfully selected. It has already been checked
     /// to not be floundering. However, it may have an answer already, be
@@ -101,6 +102,27 @@ impl<C: Context> Forest<C> {
                     ambiguous: answer.ambiguous,
                 })
             }
+            Err(RootSearchFail::Floundered) => {
+                if state.stack.is_empty() {
+                    if let Some(answer) = state.forest.tables[table].answer(answer_index) {
+                        debug!("floundered but still has answer {:?}", answer);
+                        let has_delayed_subgoals = C::has_delayed_subgoals(&answer.subst);
+                        if has_delayed_subgoals {
+                            return Err(RootSearchFail::InvalidAnswer);
+                        }
+                        Ok(CompleteAnswer {
+                            subst: C::canonical_constrained_subst_from_canonical_constrained_answer(
+                                &answer.subst,
+                            ),
+                            ambiguous: answer.ambiguous,
+                        })
+                    } else {
+                        Err(RootSearchFail::Floundered)
+                    }
+                } else {
+                    Err(RootSearchFail::Floundered)
+                }
+            }
             Err(err) => Err(err),
         }
     }
@@ -504,20 +526,18 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
                             self.on_subgoal_selected(strand)?;
                             continue;
                         }
-                        SubGoalSelection::NoRemainingSubgoals => {
-                            match self.on_no_remaining_subgoals(strand) {
+                        selection @ SubGoalSelection::NoRemainingSubgoals
+                        | selection @ SubGoalSelection::Floundered => {
+                            match self.on_no_remaining_subgoals(
+                                strand,
+                                selection == SubGoalSelection::Floundered,
+                            ) {
                                 NoRemainingSubgoalsResult::RootAnswerAvailable => return Ok(()),
                                 NoRemainingSubgoalsResult::RootSearchFail(e) => return Err(e),
                                 NoRemainingSubgoalsResult::Success => {}
                             };
                             continue;
                         }
-                        SubGoalSelection::Floundered => {
-                            // The strand floundered when trying to select a subgoal.
-                            // This will always return a `RootSearchFail`, either because the
-                            // root table floundered or we yield with `QuantumExceeded`.
-                            return Err(self.on_subgoal_selection_flounder(strand));
-                        }
                     }
                 }
                 None => {
@@ -895,10 +915,19 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
         Ok(())
     }
 
-    fn on_no_remaining_subgoals(&mut self, strand: Strand<C>) -> NoRemainingSubgoalsResult {
-        debug!("no remaining subgoals for the table");
-
-        match self.pursue_answer(strand) {
+    fn on_no_remaining_subgoals(
+        &mut self,
+        strand: Strand<C>,
+        floundered: bool,
+    ) -> NoRemainingSubgoalsResult {
+        let possible_answer = if !floundered {
+            debug!("no remaining subgoals for the table");
+            self.pursue_answer(strand)
+        } else {
+            debug!("all remaining subgoals floundered for the table");
+            self.pursue_answer_from_floundered(strand)
+        };
+        match possible_answer {
             Some(answer_index) => {
                 debug!("answer is available");
 
@@ -946,6 +975,14 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
                 }
             }
             None => {
+                if floundered {
+                    // The strand floundered when trying to select a subgoal.
+                    // This will always return a `RootSearchFail`, either because the
+                    // root table floundered or we yield with `QuantumExceeded`.
+                    return NoRemainingSubgoalsResult::RootSearchFail(
+                        self.on_subgoal_selection_flounder(),
+                    );
+                }
                 debug!("answer is not available (or not new)");
 
                 // This table ned nowhere of interest
@@ -1018,16 +1055,13 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
         Some(Forest::canonicalize_strand(self.context, strand))
     }
 
-    fn on_subgoal_selection_flounder(&mut self, strand: Strand<C>) -> RootSearchFail {
+    fn on_subgoal_selection_flounder(&mut self) -> RootSearchFail {
         debug!("all subgoals floundered");
 
         // We were unable to select a subgoal for this strand
         // because all of them had floundered or because any one
         // that we dependended on negatively floundered
 
-        // We discard this strand because it led nowhere of interest
-        drop(strand);
-
         loop {
             // This table is marked as floundered
             let table = self.stack.top().table;
@@ -1288,6 +1322,55 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
         }
     }
 
+    fn pursue_answer_from_floundered(&mut self, strand: Strand<C>) -> Option<AnswerIndex> {
+        let table = self.stack.top().table;
+        let Strand {
+            mut infer,
+            ex_clause:
+                ExClause {
+                    subst,
+                    constraints,
+                    ambiguous: _,
+                    subgoals,
+                    delayed_subgoals,
+                    answer_time: _,
+                    floundered_subgoals: _,
+                },
+            selected_subgoal: _,
+            last_pursued_time: _,
+        } = strand;
+        assert!(subgoals.is_empty());
+        let subst = infer.canonicalize_answer_subst(
+            self.context.interner(),
+            subst,
+            constraints,
+            delayed_subgoals,
+        );
+        debug!(
+            "answer from floundered goal: table={:?}, subst={:?}",
+            table, subst
+        );
+
+        let answer = Answer {
+            subst,
+            ambiguous: true,
+        };
+        let is_trivial_answer = self
+            .context
+            .is_trivial_substitution(&self.forest.tables[table].table_goal, &answer.subst);
+
+        if is_trivial_answer {
+            None
+        } else {
+            if let Some(answer_index) = self.forest.tables[table].push_answer(answer) {
+                Some(answer_index)
+            } else {
+                info!("answer: not a new answer, returning None");
+                None
+            }
+        }
+    }
+
     /// Invoked when a strand represents an **answer**. This means
     /// that the strand has no subgoals left. There are two possibilities:
     ///

chalk-solve/src/infer.rs

@@ -149,14 +149,6 @@ impl<I: Interner> InferenceTable<I> {
         Some(v1)
     }
 
-    /// 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,
-        }
-    }
-
     /// Finds the type to which `var` is bound, returning `None` if it is not yet
     /// bound.
     ///
@@ -199,36 +191,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) {
-                ParameterKind::Ty(ty) => {
-                    if let Some(var) = ty.inference_var(interner) {
-                        if self.var_is_bound(var) {
-                            return false;
-                        }
-                    }
-                }
-
-                ParameterKind::Lifetime(lifetime) => {
-                    if let Some(var) = lifetime.inference_var(interner) {
-                        if self.var_is_bound(var) {
-                            return false;
-                        }
-                    }
-                }
-            }
-        }
-
-        true
-    }
 }
 
 pub(crate) trait ParameterEnaVariableExt<I: Interner> {

chalk-solve/src/recursive/fulfill.rs

@@ -421,8 +421,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
@@ -439,10 +440,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,
+                        )));
                     }
                 }
             }

chalk-solve/src/solve/slg.rs

@@ -275,6 +275,14 @@ impl<'me, I: Interner> context::ContextOps<SlgContext<I>> for SlgContextOps<'me,
         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>>>,

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

@@ -40,9 +40,13 @@ impl<I: Interner> context::AggregateOps<SlgContext<I>> for SlgContextOps<'_, I>
         // 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));

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 [] }"
+        }
+    }
+}

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 [] })"
         }
     }
 }