Pass canonical goals to program clauses code in SLG solver

chalk-engine/src/logic.rs

@@ -12,8 +12,8 @@ use crate::{
 
 use chalk_ir::interner::Interner;
 use chalk_ir::{
-    AnswerSubst, Canonical, CanonicalVarKinds, ConstrainedSubst, FallibleOrFloundered, Floundered,
-    Goal, GoalData, InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap,
+    AnswerSubst, Canonical, ConstrainedSubst, FallibleOrFloundered, Floundered, Goal, GoalData,
+    InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap,
 };
 use chalk_solve::clauses::program_clauses_for_goal;
 use chalk_solve::coinductive_goal::IsCoinductive;
@@ -253,24 +253,30 @@ impl<I: Interner> Forest<I> {
     ) -> Table<I> {
         let coinductive = goal.is_coinductive(context.program());
         let mut table = Table::new(goal.clone(), coinductive);
-        let (infer, subst, InEnvironment { environment, goal }) =
-            chalk_solve::infer::InferenceTable::from_canonical(
-                context.program().interner(),
-                goal.universes,
-                goal.canonical,
-            );
-        let mut infer = TruncatingInferenceTable::new(context.max_size(), infer);
-        let goal_data = goal.data(context.program().interner());
 
+        let goal_data = goal.canonical.value.goal.data(context.program().interner());
         match goal_data {
             GoalData::DomainGoal(domain_goal) => {
                 let program = context.program();
-                let clauses = program_clauses_for_goal(
-                    program,
-                    &environment,
-                    &domain_goal,
-                    &CanonicalVarKinds::empty(program.interner()),
-                );
+
+                let canon_domain_goal = UCanonical {
+                    canonical: Canonical {
+                        binders: goal.canonical.binders,
+                        value: InEnvironment::new(
+                            &goal.canonical.value.environment,
+                            domain_goal.clone(),
+                        ),
+                    },
+                    universes: goal.universes,
+                };
+                let clauses = program_clauses_for_goal(program, &canon_domain_goal);
+                let (infer, subst, InEnvironment { environment, goal }) =
+                    chalk_solve::infer::InferenceTable::from_canonical(
+                        context.program().interner(),
+                        canon_domain_goal.universes,
+                        canon_domain_goal.canonical,
+                    );
+                let infer = TruncatingInferenceTable::new(context.max_size(), infer);
 
                 match clauses {
                     Ok(clauses) => {
@@ -281,7 +287,7 @@ impl<I: Interner> Forest<I> {
                                 context.unification_database(),
                                 context.program().interner(),
                                 &environment,
-                                &domain_goal,
+                                &goal,
                                 &subst,
                                 &clause,
                             ) {
@@ -309,13 +315,19 @@ impl<I: Interner> Forest<I> {
             }
 
             _ => {
-                // `canonical_goal` is a goal. We can simplify it
-                // into a series of *literals*, all of which must be
-                // true. Thus, in EWFS terms, we are effectively
-                // creating a single child of the `A :- A` goal that
-                // is like `A :- B, C, D` where B, C, and D are the
-                // simplified subgoals. You can think of this as
-                // applying built-in "meta program clauses" that
+                let (infer, subst, InEnvironment { environment, goal }) =
+                    chalk_solve::infer::InferenceTable::from_canonical(
+                        context.program().interner(),
+                        goal.universes,
+                        goal.canonical,
+                    );
+                let mut infer = TruncatingInferenceTable::new(context.max_size(), infer);
+                // The goal for this table is not a domain goal, so we instead
+                // simplify it into a series of *literals*, all of which must be
+                // true. Thus, in EWFS terms, we are effectively creating a
+                // single child of the `A :- A` goal that is like `A :- B, C, D`
+                // where B, C, and D are the simplified subgoals. You can think
+                // of this as applying built-in "meta program clauses" that
                 // reduce goals into Domain goals.
                 match Self::simplify_goal(context, &mut infer, subst, environment, goal) {
                     FallibleOrFloundered::Ok(ex_clause) => {

chalk-recursive/src/solve.rs

@@ -205,12 +205,7 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
         &self,
         canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
     ) -> Result<Vec<ProgramClause<I>>, Floundered> {
-        program_clauses_for_goal(
-            self.db(),
-            &canonical_goal.canonical.value.environment,
-            &canonical_goal.canonical.value.goal,
-            &canonical_goal.canonical.binders,
-        )
+        program_clauses_for_goal(self.db(), &canonical_goal)
     }
 }
 

chalk-solve/src/clauses.rs

@@ -344,24 +344,28 @@ pub fn push_auto_trait_impls_generator_witness<I: Interner>(
 #[instrument(level = "debug", skip(db))]
 pub fn program_clauses_for_goal<'db, I: Interner>(
     db: &'db dyn RustIrDatabase<I>,
-    environment: &Environment<I>,
-    goal: &DomainGoal<I>,
-    binders: &CanonicalVarKinds<I>,
+    goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
 ) -> Result<Vec<ProgramClause<I>>, Floundered> {
     let interner = db.interner();
 
     let custom_clauses = db.custom_clauses().into_iter();
-    let clauses_that_could_match = program_clauses_that_could_match(db, environment, goal, binders)
-        .map(|cl| cl.into_iter())?;
+    let clauses_that_could_match =
+        program_clauses_that_could_match(db, goal).map(|cl| cl.into_iter())?;
 
     let clauses: Vec<ProgramClause<I>> = custom_clauses
         .chain(clauses_that_could_match)
         .chain(
-            db.program_clauses_for_env(environment)
+            db.program_clauses_for_env(&goal.canonical.value.environment)
                 .iter(interner)
                 .cloned(),
         )
-        .filter(|c| c.could_match(interner, db.unification_database(), goal))
+        .filter(|c| {
+            c.could_match(
+                interner,
+                db.unification_database(),
+                &goal.canonical.value.goal,
+            )
+        })
         .collect();
 
     debug!(?clauses);
@@ -373,21 +377,24 @@ pub fn program_clauses_for_goal<'db, I: Interner>(
 /// `goal`. This can be any superset of the correct set, but the
 /// more precise you can make it, the more efficient solving will
 /// be.
-#[instrument(level = "debug", skip(db, environment))]
+#[instrument(level = "debug", skip(db))]
 fn program_clauses_that_could_match<I: Interner>(
     db: &dyn RustIrDatabase<I>,
-    environment: &Environment<I>,
-    goal: &DomainGoal<I>,
-    // FIXME: These are the binders for `goal`. We're passing them separately
-    // because `goal` is not necessarily canonicalized: The recursive solver
-    // passes the canonical goal; the SLG solver instantiates the goal first.
-    // (See #568.)
-    binders: &CanonicalVarKinds<I>,
+    goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
 ) -> Result<Vec<ProgramClause<I>>, Floundered> {
     let interner = db.interner();
     let mut clauses: Vec<ProgramClause<I>> = vec![];
     let builder = &mut ClauseBuilder::new(db, &mut clauses);
 
+    let UCanonical {
+        canonical:
+            Canonical {
+                value: InEnvironment { environment, goal },
+                binders,
+            },
+        universes: _,
+    } = goal;
+
     match goal {
         DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => {
             let self_ty = trait_ref.self_type_parameter(interner);
@@ -396,6 +403,9 @@ fn program_clauses_that_could_match<I: Interner>(
             let trait_datum = db.trait_datum(trait_id);
 
             match self_ty.kind(interner) {
+                TyKind::InferenceVar(_, _) => {
+                    panic!("Inference vars not allowed when getting program clauses")
+                }
                 TyKind::Alias(alias) => {
                     // An alias could normalize to anything, including `dyn trait`
                     // or an opaque type, so push a clause that asks for the
@@ -583,6 +593,9 @@ fn program_clauses_that_could_match<I: Interner>(
                 let trait_datum = db.trait_datum(trait_id);
 
                 let self_ty = alias.self_type_parameter(interner);
+                if let TyKind::InferenceVar(_, _) = self_ty.kind(interner) {
+                    panic!("Inference vars not allowed when getting program clauses");
+                }
 
                 // Flounder if the self-type is unknown and the trait is non-enumerable.
                 //
@@ -840,6 +853,9 @@ fn match_ty<I: Interner>(
 ) -> Result<(), Floundered> {
     let interner = builder.interner();
     Ok(match ty.kind(interner) {
+        TyKind::InferenceVar(_, _) => {
+            panic!("Inference vars not allowed when getting program clauses")
+        }
         TyKind::Adt(adt_id, _) => builder
             .db
             .adt_datum(*adt_id)
@@ -883,7 +899,7 @@ fn match_ty<I: Interner>(
         TyKind::Function(_quantified_ty) => {
             builder.push_fact(WellFormed::Ty(ty.clone()));
         }
-        TyKind::BoundVar(_) | TyKind::InferenceVar(_, _) => return Err(Floundered),
+        TyKind::BoundVar(_) => return Err(Floundered),
         TyKind::Dyn(dyn_ty) => {
             // FIXME(#203)
             // - Object safety? (not needed with RFC 2027)