Merge pull request #626 from matthewjasper/slg-ambiguity

Handle cached answers correctly in any_future_answer

Author: matthewjasper

chalk-engine/src/logic.rs

@@ -117,14 +117,19 @@ impl<I: Interner> Forest<I> {
     pub(super) fn any_future_answer(
         &self,
         table: TableIndex,
-        answer: AnswerIndex,
+        mut answer_index: AnswerIndex,
         mut test: impl FnMut(&Substitution<I>) -> bool,
     ) -> bool {
-        if let Some(answer) = self.tables[table].answer(answer) {
+        // Check any cached answers, starting at `answer_index`.
+        while let Some(answer) = self.tables[table].answer(answer_index) {
             info!("answer cached = {:?}", answer);
-            return test(&answer.subst.value.subst);
+            if test(&answer.subst.value.subst) {
+                return true;
+            }
+            answer_index.increment();
         }
 
+        // Check any unsolved strands, which may give further answers.
         self.tables[table]
             .strands()
             .any(|strand| test(&strand.canonical_ex_clause.value.subst))

tests/test/numerics.rs

@@ -225,3 +225,26 @@ fn integers_are_sized() {
         }
     }
 }
+
+/// Simplified version of a goal that needs to be solved for type checking
+/// `1 + 2`.
+#[test]
+fn ambiguous_add() {
+    test! {
+        program {
+            #[non_enumerable]
+            trait Add<Rhs> { type Output; }
+
+            impl<'a> Add<&'a u32> for u32 { type Output = <u32 as Add<u32>>::Output; }
+            impl Add<u32> for u32 { type Output = u32; }
+        }
+
+        goal {
+            exists<int T, U, V> {
+                <T as Add<U>>::Output = V
+            }
+        } yields {
+            "Ambiguous; no inference guidance"
+        }
+    }
+}