expand coinductive reasoning

Author: nikomatsakis

chalk-engine/src/logic.rs

@@ -1487,8 +1487,13 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
     /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is
     /// false, since `XXX` is not an auto trait.
     pub(super) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool {
+        debug_heading!("top_of_stack_is_coinductive_from(depth={:?})", depth);
         StackIndex::iterate_range(self.stack.top_of_stack_from(depth)).all(|d| {
             let table = self.stack[d].table;
+            debug!(
+                "d = {:?}, table = {:?}",
+                d, self.forest.tables[table].table_goal
+            );
             self.forest.tables[table].coinductive_goal
         })
     }

chalk-solve/src/clauses.rs

@@ -243,9 +243,15 @@ fn program_clauses_that_could_match<I: Interner>(
                 .opaque_ty_data(opaque_ty.opaque_ty_id)
                 .to_program_clauses(builder),
         },
-        DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
-        | DomainGoal::LocalImplAllowed(trait_ref) => {
-            db.trait_datum(trait_ref.trait_id)
+        DomainGoal::LocalImplAllowed(trait_ref) => db
+            .trait_datum(trait_ref.trait_id)
+            .to_program_clauses(builder),
+        DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => {
+            let self_ty = trait_predicate.self_type_parameter(interner);
+            if self_ty.bound_var(interner).is_some() || self_ty.inference_var(interner).is_some() {
+                return Err(Floundered);
+            }
+            db.trait_datum(trait_predicate.trait_id)
                 .to_program_clauses(builder);
         }
         DomainGoal::ObjectSafe(trait_id) => {

chalk-solve/src/coinductive_goal.rs

@@ -15,6 +15,18 @@ pub trait IsCoinductive<I: Interner> {
 }
 
 impl<I: Interner> IsCoinductive<I> for Goal<I> {
+    /// A "coinductive" goal `G` is a goal where `G :- G` should be considered
+    /// true. When we are doing trait solving, if we encounter a cycle of goals
+    /// where solving `G1` requires `G2..Gn` and solving `Gn` requires `G1`,
+    /// then our behavior depends on whether each goal `Gi` in that cycle is
+    /// coinductive.
+    ///
+    /// If all the goals are coinductive, then `G1` is considered provable,
+    /// presuming that all the other subgoals for `G2..Gn` within can be fully
+    /// proven.
+    ///
+    /// If any goal `Gi` in the cycle is inductive, however, then the cycle is
+    /// considered unprovable.
     fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool {
         let interner = db.interner();
         match self.data(interner) {
@@ -26,10 +38,33 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
                 WhereClause::AliasEq(..) => false,
             },
             GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
-            GoalData::Quantified(QuantifierKind::ForAll, goal) => {
-                goal.skip_binders().is_coinductive(db)
-            }
-            _ => false,
+            GoalData::DomainGoal(_) => false,
+
+            // Goals like `forall<..> { G }` or `... => G` we will consider to
+            // be coinductive if G is coinductive, although in practice I think
+            // it would be ok to simply consider them coinductive all the time.
+            GoalData::Quantified(_, goal) => goal.skip_binders().is_coinductive(db),
+            GoalData::Implies(_, goal) => goal.is_coinductive(db),
+
+            // The "All(...)" quantifier is considered coinductive. This could
+            // be somewhat surprising as you might have `All(Gc, Gi)` where `Gc`
+            // is coinductive and `Gi` is inductive. This however is really no
+            // different than defining a fresh coinductive goal like
+            //
+            // ```notrust
+            // Gx :- Gc, Gi
+            // ```
+            //
+            // and requiring `Gx` in place of `All(Gc, Gi)`, and that would be
+            // perfectly reasonable.
+            GoalData::All(..) => true,
+
+            // For simplicity, just assume these remaining types of goals must
+            // be inductive, since there is no pressing reason to consider them
+            // coinductive.
+            GoalData::Not(_) => false,
+            GoalData::EqGoal(_) => false,
+            GoalData::CannotProve(_) => false,
         }
     }
 }