add correct handling of false positives in coinductive cycles

add new tests for coinduction handling

Author: firefighterduck

chalk-recursive/src/recursive.rs

@@ -224,20 +224,33 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
             // Check if this table is still on the stack.
             if let Some(depth) = self.context.search_graph[dfn].stack_depth {
                 // Is this a coinductive goal? If so, that is success,
-                // so we can return normally. Note that this return is
-                // not tabled.
-                //
-                // XXX how does caching with coinduction work?
+                // so we can return and set the minimum to its DFN.
+                // Note that this return is not tabled. And so are
+                // all other solutions in the cycle until the cycle
+                // start is finished. This avoids prematurely cached
+                // false positives.
                 if self.context.stack.coinductive_cycle_from(depth) {
                     let value = ConstrainedSubst {
                         subst: goal.trivial_substitution(self.program.interner()),
                         constraints: Constraints::empty(self.program.interner()),
                     };
-                    debug!("applying coinductive semantics");
-                    return Ok(Solution::Unique(Canonical {
+                    let trivial_solution = Ok(Solution::Unique(Canonical {
                         value,
                         binders: goal.canonical.binders,
                     }));
+
+                    debug!("applying coinductive semantics");
+
+                    // Set minimum to first occurrence of cyclic goal to prevent premature caching of possibly false solutions
+                    minimums.update_from(self.context.search_graph[dfn].links);
+
+                    // Store trivial solution to start coinductive reasoning from this node
+                    self.context.search_graph[dfn].solution = trivial_solution.clone();
+                    self.context.search_graph[dfn].solution_priority =
+                        chalk_ir::ClausePriority::Low;
+                    self.context.search_graph[dfn].coinductive_start = true;
+
+                    return trivial_solution;
                 }
 
                 self.context.stack[depth].flag_cycle();
@@ -275,6 +288,11 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
             // worst of the repeated work that we do during tabling.
             if subgoal_minimums.positive >= dfn {
                 if self.context.caching_enabled {
+                    // Remove possible false positives from coinductive cycle
+                    if self.context.search_graph[dfn].coinductive_start && result.is_err() {
+                        self.context.search_graph.remove_false_positives_after(dfn);
+                    }
+
                     self.context
                         .search_graph
                         .move_to_cache(dfn, &mut self.context.cache);

chalk-recursive/src/search_graph.rs

@@ -37,6 +37,11 @@ pub(super) struct Node<I: Interner> {
     /// from the stack, it contains the DFN of the minimal ancestor
     /// that the table reached (or MAX if no cycle was encountered).
     pub(crate) links: Minimums,
+
+    /// If this is true, the node is the start of coinductive cycle.
+    /// Thus, some cleanup has to be done before its result can be
+    /// cached to rule out false positives.
+    pub(crate) coinductive_start: bool,
 }
 
 impl<I: Interner> SearchGraph<I> {
@@ -71,6 +76,7 @@ impl<I: Interner> SearchGraph<I> {
             solution_priority: ClausePriority::High,
             stack_depth: Some(stack_depth),
             links: Minimums { positive: dfn },
+            coinductive_start: false,
         };
         self.nodes.push(node);
         let previous_index = self.indices.insert(goal.clone(), dfn);
@@ -101,6 +107,32 @@ impl<I: Interner> SearchGraph<I> {
             cache.insert(node.goal, node.solution);
         }
     }
+
+    /// Removes all nodes that are part of a coinductive cycle and
+    /// have a solution as they might be false positives due to
+    /// coinductive reasoning.
+    #[instrument(level = "debug", skip(self))]
+    pub(crate) fn remove_false_positives_after(&mut self, dfn: DepthFirstNumber) {
+        let mut false_positive_indices = vec![];
+
+        // Find all possible false positives in the graph below the
+        // start of the coinductive cycle
+        for (index, node) in self.nodes[dfn.index + 1..].iter().enumerate() {
+            if node.solution.is_ok() {
+                false_positive_indices.push(index + dfn.index + 1);
+            }
+        }
+
+        // Remove the potential false positives from the indices
+        self.indices
+            .retain(|_key, value| !false_positive_indices.contains(&value.index));
+
+        // Remove the potential false positives from the nodes
+        // in descending order to avoid unnecessary shifts
+        for false_positive_index in false_positive_indices.into_iter().rev() {
+            self.nodes.remove(false_positive_index);
+        }
+    }
 }
 
 impl<I: Interner> Index<DepthFirstNumber> for SearchGraph<I> {

tests/test/coinduction.rs

@@ -213,23 +213,58 @@ fn coinductive_unsound1() {
 
         goal {
             forall<X> { X: C1orC2 }
-        } yields[SolverChoice::slg(3, None)] {
+        } yields {
             "No possible solution"
         }
+    }
+}
+
+/// The only difference between this test and `coinductive_unsound1`
+/// is the order of the final `forall` clauses.
+#[test]
+fn coinductive_unsound2() {
+    test! {
+        program {
+            trait C1orC2 { }
+
+            #[coinductive]
+            trait C1 { }
+
+            #[coinductive]
+            trait C2 { }
+
+            #[coinductive]
+            trait C3 { }
+
+            forall<T> {
+                T: C1 if T: C2, T: C3
+            }
+
+            forall<T> {
+                T: C2 if T: C1
+            }
+
+            forall<T> {
+                T: C1orC2 if T: C2
+            }
+
+            forall<T> {
+                T: C1orC2 if T: C1
+            }
+        }
 
         goal {
             forall<X> { X: C1orC2 }
-        } yields[SolverChoice::recursive_default()] {
-            // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly
-            "Unique; substitution [], lifetime constraints []"
+        } yields {
+            "No possible solution"
         }
     }
 }
 
-/// The only difference between this test and `coinductive_unsound1`
-/// is the order of the final `forall` clauses.
+/// Same as the two before but needs to show T: C2 in both
+// branches of T: C1.
 #[test]
-fn coinductive_unsound2() {
+fn coinductive_unsound3() {
     test! {
         program {
             trait C1orC2 { }
@@ -243,6 +278,13 @@ fn coinductive_unsound2() {
             #[coinductive]
             trait C3 { }
 
+            #[coinductive]
+            trait C4 { }
+
+            forall<T> {
+                T: C3 if T: C2, T: C4
+            }
+
             forall<T> {
                 T: C1 if T: C2, T: C3
             }
@@ -251,13 +293,62 @@ fn coinductive_unsound2() {
                 T: C2 if T: C1
             }
 
+            forall<T> {
+                T: C1orC2 if T: C1
+            }
+
             forall<T> {
                 T: C1orC2 if T: C2
             }
+        }
+
+        goal {
+            forall<X> { X: C1orC2 }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
+/// Tests whether a nested coinductive cycle
+/// that is also unsound is handled correctly.
+#[test]
+fn coinductive_unsound4() {
+    test! {
+        program {
+            trait C1orC2 { }
+
+            #[coinductive]
+            trait C1 { }
+
+            #[coinductive]
+            trait C2 { }
+
+            #[coinductive]
+            trait C3 { }
+
+            #[coinductive]
+            trait C4 { }
+
+            forall<T> {
+                T: C4 if T:C2, T: C3
+            }
+
+            forall<T> {
+                T: C1 if T: C2, T: C3
+            }
+
+            forall<T> {
+                T: C2 if T: C1, T: C4
+            }
 
             forall<T> {
                 T: C1orC2 if T: C1
             }
+
+            forall<T> {
+                T: C1orC2 if T: C2
+            }
         }
 
         goal {
@@ -450,14 +541,8 @@ fn coinductive_multicycle4() {
 
         goal {
             forall<X> { X: Any }
-        } yields_all[SolverChoice::slg(3, None)] {
-        }
-
-        goal {
-            forall<X> { X: Any }
-        } yields[SolverChoice::recursive_default()] {
-            // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly
-            "Unique; substitution [], lifetime constraints []"
+        } yields {
+            "No possible solution"
         }
     }
 }