encapsulate the coinductive logic into chalk-solve

This also removes the need to work around the lack of trait object
upcasts.

Author: nikomatsakis

chalk-ir/src/lib.rs

@@ -53,14 +53,6 @@ pub mod tls;
 
 pub type Identifier = InternedString;
 
-pub trait IsCoinductive {
-    /// Convert to a dyn trait value representing `self`. This is a
-    /// workaround for the lack of proper upcasting in Rust.
-    fn as_dyn(&self) -> &dyn IsCoinductive;
-
-    fn is_coinductive_trait(&self, trait_id: TraitId) -> bool;
-}
-
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
 /// The set of assumptions we've made so far, and the current number of
 /// universal (forall) quantifiers we're within.
@@ -925,16 +917,6 @@ impl<T> UCanonical<T> {
     }
 }
 
-impl UCanonical<InEnvironment<Goal>> {
-    /// A goal has coinductive semantics if it is of the form `T: AutoTrait`, or if it is of the
-    /// form `WellFormed(T: Trait)` where `Trait` is any trait. The latter is needed for dealing
-    /// with WF requirements and cyclic traits, which generates cycles in the proof tree which must
-    /// not be rejected but instead must be treated as a success.
-    pub fn is_coinductive(&self, program: &dyn IsCoinductive) -> bool {
-        self.canonical.value.goal.is_coinductive(program)
-    }
-}
-
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
 /// A general goal; this is the full range of questions you can pose to Chalk.
 pub enum Goal {
@@ -999,18 +981,6 @@ impl Goal {
     pub fn implied_by(self, predicates: Vec<ProgramClause>) -> Goal {
         Goal::Implies(predicates, Box::new(self))
     }
-
-    pub fn is_coinductive(&self, program: &dyn IsCoinductive) -> bool {
-        match self {
-            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Holds(wca))) => match wca {
-                WhereClause::Implemented(tr) => program.is_coinductive_trait(tr.trait_id),
-                WhereClause::ProjectionEq(..) => false,
-            },
-            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..)))) => true,
-            Goal::Quantified(QuantifierKind::ForAll, goal) => goal.value.is_coinductive(program),
-            _ => false,
-        }
-    }
 }
 
 #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]

chalk-rules/src/lib.rs

@@ -19,10 +19,6 @@ pub trait GoalSolver {
 }
 
 pub trait RustIrSource {
-    /// Convert to a dyn trait value representing `self`. This is a
-    /// workaround for the lack of proper upcasting in Rust.
-    fn as_dyn(&self) -> &dyn RustIrSource;
-
     /// Returns the datum for the associated type with the given id.
     fn associated_ty_data(&self, ty: TypeId) -> Arc<AssociatedTyDatum>;
 

chalk-solve/src/coinductive_goal.rs

@@ -0,0 +1,34 @@
+use crate::ChalkSolveDatabase;
+use chalk_ir::*;
+
+pub trait IsCoinductive {
+    /// A goal G has coinductive semantics if proving G is allowed to
+    /// assume G is true (very roughly speaking). In the case of
+    /// chalk-ir, this is true for goals of the form `T: AutoTrait`,
+    /// or if it is of the form `WellFormed(T: Trait)` where `Trait`
+    /// is any trait. The latter is needed for dealing with WF
+    /// requirements and cyclic traits, which generates cycles in the
+    /// proof tree which must not be rejected but instead must be
+    /// treated as a success.
+    fn is_coinductive(&self, db: &dyn ChalkSolveDatabase) -> bool;
+}
+
+impl IsCoinductive for Goal {
+    fn is_coinductive(&self, db: &dyn ChalkSolveDatabase) -> bool {
+        match self {
+            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Holds(wca))) => match wca {
+                WhereClause::Implemented(tr) => db.is_coinductive_trait(tr.trait_id),
+                WhereClause::ProjectionEq(..) => false,
+            },
+            Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..)))) => true,
+            Goal::Quantified(QuantifierKind::ForAll, goal) => goal.value.is_coinductive(db),
+            _ => false,
+        }
+    }
+}
+
+impl IsCoinductive for UCanonical<InEnvironment<Goal>> {
+    fn is_coinductive(&self, db: &dyn ChalkSolveDatabase) -> bool {
+        self.canonical.value.goal.is_coinductive(db)
+    }
+}

chalk-solve/src/lib.rs

@@ -1,13 +1,26 @@
+use chalk_ir::{DomainGoal, ProgramClause, TraitId};
+use std::fmt::Debug;
+
 #[macro_use]
 extern crate chalk_macros;
-extern crate chalk_engine;
-extern crate chalk_ir;
 
+mod coinductive_goal;
 pub mod ext;
 mod infer;
 mod solve;
 
-pub use solve::ChalkSolveDatabase;
+/// The trait for defining the program clauses that are in scope when
+/// solving a goal.
+pub trait ChalkSolveDatabase: Debug {
+    /// Returns a set of program clauses that could possibly match
+    /// `goal`. This can be any superset of the correct set, but the
+    /// more precise you can make it, the more efficient solving will
+    /// be.
+    fn program_clauses_that_could_match(&self, goal: &DomainGoal, vec: &mut Vec<ProgramClause>);
+
+    fn is_coinductive_trait(&self, trait_id: TraitId) -> bool;
+}
+
 pub use solve::Solution;
 pub use solve::Solver;
 pub use solve::SolverChoice;

chalk-solve/src/solve.rs

@@ -1,11 +1,8 @@
 use crate::solve::slg::SlgContext;
+use crate::ChalkSolveDatabase;
 use chalk_engine::forest::Forest;
-use chalk_ir::DomainGoal;
-use chalk_ir::IsCoinductive;
-use chalk_ir::ProgramClause;
 use chalk_ir::*;
 use std::fmt;
-use std::fmt::Debug;
 
 mod slg;
 mod truncate;
@@ -187,17 +184,3 @@ impl TestSolver {
         self.forest.num_cached_answers_for_goal(&ops, goal)
     }
 }
-
-/// The trait for defining the program clauses that are in scope when
-/// solving a goal.
-pub trait ChalkSolveDatabase: Debug + IsCoinductive {
-    /// Convert to a dyn trait value representing `self`. This is a
-    /// workaround for the lack of proper upcasting in Rust.
-    fn as_dyn(&self) -> &dyn ChalkSolveDatabase;
-
-    /// Returns a set of program clauses that could possibly match
-    /// `goal`. This can be any superset of the correct set, but the
-    /// more precise you can make it, the more efficient solving will
-    /// be.
-    fn program_clauses_that_could_match(&self, goal: &DomainGoal, vec: &mut Vec<ProgramClause>);
-}

chalk-solve/src/solve/slg.rs

@@ -1,9 +1,10 @@
+use crate::coinductive_goal::IsCoinductive;
 use crate::infer::ucanonicalize::{UCanonicalized, UniverseMap};
 use crate::infer::unify::UnificationResult;
 use crate::infer::InferenceTable;
 use crate::solve::truncate::{self, Truncated};
-use crate::solve::ChalkSolveDatabase;
 use crate::solve::Solution;
+use crate::ChalkSolveDatabase;
 use chalk_engine::fallible::Fallible;
 use chalk_ir::cast::{Cast, Caster};
 use chalk_ir::could_match::CouldMatch;
@@ -120,7 +121,7 @@ impl context::Context for SlgContext {
 
 impl<'me> context::ContextOps<SlgContext> for SlgContextOps<'me> {
     fn is_coinductive(&self, goal: &UCanonical<InEnvironment<Goal>>) -> bool {
-        goal.is_coinductive(IsCoinductive::as_dyn(self.program))
+        goal.is_coinductive(self.program)
     }
 
     fn instantiate_ucanonical_goal<R>(

src/db.rs

@@ -9,7 +9,6 @@ use chalk_ir::Goal;
 use chalk_ir::Identifier;
 use chalk_ir::ImplId;
 use chalk_ir::InEnvironment;
-use chalk_ir::IsCoinductive;
 use chalk_ir::Parameter;
 use chalk_ir::ProgramClause;
 use chalk_ir::ProjectionTy;
@@ -65,10 +64,6 @@ impl ChalkDatabase {
 }
 
 impl ChalkSolveDatabase for ChalkDatabase {
-    fn as_dyn(&self) -> &dyn ChalkSolveDatabase {
-        self
-    }
-
     fn program_clauses_that_could_match(&self, goal: &DomainGoal, vec: &mut Vec<ProgramClause>) {
         if let Ok(env) = self.environment() {
             vec.extend(
@@ -79,12 +74,6 @@ impl ChalkSolveDatabase for ChalkDatabase {
             );
         }
     }
-}
-
-impl IsCoinductive for ChalkDatabase {
-    fn as_dyn(&self) -> &dyn IsCoinductive {
-        self
-    }
 
     fn is_coinductive_trait(&self, trait_id: TraitId) -> bool {
         if let Ok(env) = self.environment() {
@@ -96,10 +85,6 @@ impl IsCoinductive for ChalkDatabase {
 }
 
 impl RustIrSource for ChalkDatabase {
-    fn as_dyn(&self) -> &dyn RustIrSource {
-        self
-    }
-
     fn associated_ty_data(&self, ty: TypeId) -> Arc<AssociatedTyDatum> {
         self.program_ir().unwrap().associated_ty_data[&ty].clone()
     }