From cc4778e961121343600dc0af8d42a5de685ec6c3 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Tue, 29 Sep 2020 15:35:00 -0400 Subject: [PATCH 1/3] Find program clauses for canonical goals in SLG Instead of instantiating goals first, as is the case currently --- chalk-engine/src/logic.rs | 46 +++++++++++++++++++++++++++------------ 1 file changed, 32 insertions(+), 14 deletions(-) diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index 6c0f102d756..73e11e5044f 100644 --- a/chalk-engine/src/logic.rs +++ b/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,35 @@ impl Forest { ) -> Table { 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 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, - &environment, - &domain_goal, - &CanonicalVarKinds::empty(program.interner()), + &canon_domain_goal.canonical.value.environment, + &canon_domain_goal.canonical.value.goal, + &canon_domain_goal.canonical.binders, ); + 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 +292,7 @@ impl Forest { context.unification_database(), context.program().interner(), &environment, - &domain_goal, + &goal, &subst, &clause, ) { @@ -309,6 +320,13 @@ impl Forest { } _ => { + 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); // `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 From d719618f8e57a18006b40966253d96ec36be63cc Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Fri, 9 Oct 2020 19:35:53 -0400 Subject: [PATCH 2/3] Simplify program clause methods --- chalk-engine/src/logic.rs | 7 +------ chalk-recursive/src/solve.rs | 7 +------ chalk-solve/src/clauses.rs | 37 +++++++++++++++++++++--------------- 3 files changed, 24 insertions(+), 27 deletions(-) diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index 73e11e5044f..504f03d726e 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -269,12 +269,7 @@ impl Forest { }, universes: goal.universes, }; - let clauses = program_clauses_for_goal( - program, - &canon_domain_goal.canonical.value.environment, - &canon_domain_goal.canonical.value.goal, - &canon_domain_goal.canonical.binders, - ); + 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(), diff --git a/chalk-recursive/src/solve.rs b/chalk-recursive/src/solve.rs index fc3584abfda..7fdf725dd42 100644 --- a/chalk-recursive/src/solve.rs +++ b/chalk-recursive/src/solve.rs @@ -205,12 +205,7 @@ trait SolveIterationHelpers: SolveDatabase { &self, canonical_goal: &UCanonical>>, ) -> Result>, 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) } } diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index a9080ef4efc..2487c3586c7 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -344,24 +344,28 @@ pub fn push_auto_trait_impls_generator_witness( #[instrument(level = "debug", skip(db))] pub fn program_clauses_for_goal<'db, I: Interner>( db: &'db dyn RustIrDatabase, - environment: &Environment, - goal: &DomainGoal, - binders: &CanonicalVarKinds, + goal: &UCanonical>>, ) -> Result>, 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> = 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( db: &dyn RustIrDatabase, - environment: &Environment, - goal: &DomainGoal, - // 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, + goal: &UCanonical>>, ) -> Result>, Floundered> { let interner = db.interner(); let mut clauses: Vec> = 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); From 0b391f8eed657ac23abad15e5d6ae9a5c7852f11 Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Tue, 8 Dec 2020 22:17:49 -0500 Subject: [PATCH 3/3] Forbid inference vars when getting program clauses --- chalk-engine/src/logic.rs | 13 ++++++------- chalk-solve/src/clauses.rs | 11 ++++++++++- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs index 504f03d726e..30cb0f1990c 100644 --- a/chalk-engine/src/logic.rs +++ b/chalk-engine/src/logic.rs @@ -322,13 +322,12 @@ impl Forest { goal.canonical, ); let mut infer = TruncatingInferenceTable::new(context.max_size(), infer); - // `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 + // 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) => { diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 2487c3586c7..ea6851338e2 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -403,6 +403,9 @@ fn program_clauses_that_could_match( 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 @@ -590,6 +593,9 @@ fn program_clauses_that_could_match( 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. // @@ -847,6 +853,9 @@ fn match_ty( ) -> 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) @@ -890,7 +899,7 @@ fn match_ty( 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)