From 126bf6faa1a0c6b64b2183178bb902d5cd49ab15 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 13:20:52 +0100 Subject: [PATCH 01/50] Add back the code for the recursive solver (not yet building) --- chalk-solve/src/lib.rs | 1 + chalk-solve/src/recursive/fulfill.rs | 418 ++++++++++++++++++++++ chalk-solve/src/recursive/mod.rs | 416 +++++++++++++++++++++ chalk-solve/src/recursive/search_graph.rs | 127 +++++++ chalk-solve/src/recursive/stack.rs | 103 ++++++ chalk-solve/src/recursive/tables.rs | 57 +++ 6 files changed, 1122 insertions(+) create mode 100644 chalk-solve/src/recursive/fulfill.rs create mode 100644 chalk-solve/src/recursive/mod.rs create mode 100644 chalk-solve/src/recursive/search_graph.rs create mode 100644 chalk-solve/src/recursive/stack.rs create mode 100644 chalk-solve/src/recursive/tables.rs diff --git a/chalk-solve/src/lib.rs b/chalk-solve/src/lib.rs index 76a9253471c..e5dc4a8d056 100644 --- a/chalk-solve/src/lib.rs +++ b/chalk-solve/src/lib.rs @@ -15,6 +15,7 @@ mod coinductive_goal; pub mod ext; pub mod goal_builder; mod infer; +pub mod recursive; mod solve; pub mod split; pub mod wf; diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs new file mode 100644 index 00000000000..c3c504819f2 --- /dev/null +++ b/chalk-solve/src/recursive/fulfill.rs @@ -0,0 +1,418 @@ +use super::*; +use cast::Caster; +use fold::Fold; +use solve::infer::{ + canonicalize::Canonicalized, + instantiate::BindersAndValue, + ucanonicalize::{UCanonicalized, UniverseMap}, + unify::UnificationResult, + InferenceTable, ParameterInferenceVariable, +}; +use std::collections::HashSet; +use std::fmt::Debug; +use std::sync::Arc; +use zip::Zip; + +enum Outcome { + Complete, + Incomplete, +} + +impl Outcome { + fn is_complete(&self) -> bool { + match *self { + Outcome::Complete => true, + _ => false, + } + } +} + +/// A goal that must be resolved +#[derive(Clone, Debug, PartialEq, Eq)] +enum Obligation { + /// For "positive" goals, we flatten all the way out to leafs within the + /// current `Fulfill` + Prove(InEnvironment), + + /// For "negative" goals, we don't flatten in *this* `Fulfill`, which would + /// require having a logical "or" operator. Instead, we recursively solve in + /// a fresh `Fulfill`. + Refute(InEnvironment), +} + +/// When proving a leaf goal, we record the free variables that appear within it +/// so that we can update inference state accordingly. +#[derive(Clone, Debug)] +struct PositiveSolution { + free_vars: Vec, + universes: UniverseMap, + solution: Solution, +} + +/// When refuting a goal, there's no impact on inference state. +#[derive(Copy, Clone, Debug, PartialEq, Eq)] +enum NegativeSolution { + Refuted, + Ambiguous, +} + +/// A `Fulfill` is where we actually break down complex goals, instantiate +/// variables, and perform inference. It's highly stateful. It's generally used +/// in Chalk to try to solve a goal, and then package up what was learned in a +/// stateless, canonical way. +/// +/// In rustc, you can think of there being an outermost `Fulfill` that's used when +/// type checking each function body, etc. There, the state reflects the state +/// of type inference in general. But when solving trait constraints, *fresh* +/// `Fulfill` instances will be created to solve canonicalized, free-standing +/// goals, and transport what was learned back to the outer context. +crate struct Fulfill<'s> { + solver: &'s mut Solver, + infer: InferenceTable, + + /// The remaining goals to prove or refute + obligations: Vec, + + /// Lifetime constraints that must be fulfilled for a solution to be fully + /// validated. + constraints: HashSet>, + + /// Record that a goal has been processed that can neither be proved nor + /// refuted. In such a case the solution will be either `CannotProve`, or `Err` + /// in the case where some other goal leads to an error. + cannot_prove: bool, +} + +impl<'s> Fulfill<'s> { + pub(crate) fn new(solver: &'s mut Solver) -> Self { + Fulfill { + solver, + infer: InferenceTable::new(), + obligations: vec![], + constraints: HashSet::new(), + cannot_prove: false, + } + } + + /// Given the canonical, initial goal, returns a substitution + /// that, when applied to this goal, will convert all of its bound + /// variables into fresh inference variables. The substitution can + /// then later be used as the answer to be returned to the user. + /// + /// See also `InferenceTable::fresh_subst`. + pub(crate) fn initial_subst>( + &mut self, + ucanonical_goal: &UCanonical>, + ) -> (Substitution, InEnvironment) { + let canonical_goal = self.infer.instantiate_universes(ucanonical_goal); + let subst = self.infer.fresh_subst(&canonical_goal.binders); + let value = canonical_goal.substitute(&subst); + (subst, value) + } + + /// Wraps `InferenceTable::instantiate_in` + #[allow(non_camel_case_types)] + pub(crate) fn instantiate_binders_existentially( + &mut self, + arg: &impl BindersAndValue, + ) -> T::Result + where + T: Fold, + { + self.infer.instantiate_binders_existentially(arg) + } + + /// Unifies `a` and `b` in the given environment. + /// + /// Wraps `InferenceTable::unify`; any resulting normalizations are added + /// into our list of pending obligations with the given environment. + pub(crate) fn unify(&mut self, environment: &Arc, a: &T, b: &T) -> Fallible<()> + where + T: ?Sized + Zip + Debug, + { + let UnificationResult { goals, constraints } = self.infer.unify(environment, a, b)?; + debug!("unify({:?}, {:?}) succeeded", a, b); + debug!("unify: goals={:?}", goals); + debug!("unify: constraints={:?}", constraints); + self.constraints.extend(constraints); + self.obligations + .extend(goals.into_iter().casted().map(Obligation::Prove)); + Ok(()) + } + + /// Create obligations for the given goal in the given environment. This may + /// ultimately create any number of obligations. + pub(crate) fn push_goal(&mut self, environment: &Arc, goal: Goal) -> Fallible<()> { + debug!("push_goal({:?}, {:?})", goal, environment); + match goal { + Goal::Quantified(QuantifierKind::ForAll, subgoal) => { + let subgoal = self.infer.instantiate_binders_universally(&subgoal); + self.push_goal(environment, *subgoal)?; + } + Goal::Quantified(QuantifierKind::Exists, subgoal) => { + let subgoal = self.infer.instantiate_binders_existentially(&subgoal); + self.push_goal(environment, *subgoal)?; + } + Goal::Implies(wc, subgoal) => { + let new_environment = &environment.add_clauses(wc); + self.push_goal(new_environment, *subgoal)?; + } + Goal::And(subgoal1, subgoal2) => { + self.push_goal(environment, *subgoal1)?; + self.push_goal(environment, *subgoal2)?; + } + Goal::Not(subgoal) => { + let in_env = InEnvironment::new(environment, *subgoal); + self.obligations.push(Obligation::Refute(in_env)); + } + Goal::Leaf(LeafGoal::DomainGoal(_)) => { + let in_env = InEnvironment::new(environment, goal); + self.obligations.push(Obligation::Prove(in_env)); + } + Goal::Leaf(LeafGoal::EqGoal(EqGoal { a, b })) => { + self.unify(&environment, &a, &b)?; + } + Goal::CannotProve(()) => { + self.cannot_prove = true; + } + } + Ok(()) + } + + fn prove( + &mut self, + wc: &InEnvironment, + minimums: &mut Minimums, + ) -> Fallible { + let Canonicalized { + quantified, + free_vars, + max_universe: _, + } = self.infer.canonicalize(wc); + let UCanonicalized { + quantified, + universes, + } = self.infer.u_canonicalize(&quantified); + Ok(PositiveSolution { + free_vars, + universes, + solution: self.solver.solve_goal(quantified, minimums)?, + }) + } + + fn refute(&mut self, goal: &InEnvironment) -> Fallible { + let canonicalized = match self.infer.invert_then_canonicalize(goal) { + Some(v) => v, + None => { + // Treat non-ground negatives as ambiguous. Note that, as inference + // proceeds, we may wind up with more information here. + return Ok(NegativeSolution::Ambiguous); + } + }; + + // Negate the result + let UCanonicalized { + quantified, + universes: _, + } = self.infer.u_canonicalize(&canonicalized); + let mut minimums = Minimums::new(); // FIXME -- minimums here seems wrong + if let Ok(solution) = self.solver.solve_goal(quantified, &mut minimums) { + if solution.is_unique() { + Err(NoSolution) + } else { + Ok(NegativeSolution::Ambiguous) + } + } else { + Ok(NegativeSolution::Refuted) + } + } + + /// Trying to prove some goal led to a the substitution `subst`; we + /// wish to apply that substitution to our own inference variables + /// (and incorporate any region constraints). This substitution + /// requires some mapping to get it into our namespace -- first, + /// the universes it refers to have been canonicalized, and + /// `universes` stores the mapping back into our + /// universes. Second, the free variables that appear within can + /// be mapped into our variables with `free_vars`. + fn apply_solution( + &mut self, + free_vars: Vec, + universes: UniverseMap, + subst: Canonical, + ) { + let subst = universes.map_from_canonical(&subst); + let ConstrainedSubst { subst, constraints } = self.infer.instantiate_canonical(&subst); + + debug!( + "fulfill::apply_solution: adding constraints {:?}", + constraints + ); + self.constraints.extend(constraints); + + // We use the empty environment for unification here because we're + // really just doing a substitution on unconstrained variables, which is + // guaranteed to succeed without generating any new constraints. + let empty_env = &Environment::new(); + + for (i, free_var) in free_vars.into_iter().enumerate() { + let subst_value = &subst.parameters[i]; + let free_value = free_var.to_parameter(); + self.unify(empty_env, &free_value, subst_value) + .unwrap_or_else(|err| { + panic!( + "apply_solution failed with free_var={:?}, subst_value={:?}: {:?}", + free_var, subst_value, err + ); + }); + } + } + + fn fulfill(&mut self, minimums: &mut Minimums) -> Fallible { + debug_heading!("fulfill(obligations={:#?})", self.obligations); + + // Try to solve all the obligations. We do this via a fixed-point + // iteration. We try to solve each obligation in turn. Anything which is + // successful, we drop; anything ambiguous, we retain in the + // `obligations` array. This process is repeated so long as we are + // learning new things about our inference state. + let mut obligations = Vec::with_capacity(self.obligations.len()); + let mut progress = true; + + while progress { + progress = false; + debug_heading!("start of round, {} obligations", self.obligations.len()); + + // Take the list of `obligations` to solve this round and replace it + // with an empty vector. Iterate through each obligation to solve + // and solve it if we can. If not (because of ambiguity), then push + // it back onto `self.to_prove` for next round. Note that + // `solve_one` may also push onto the `self.to_prove` list + // directly. + assert!(obligations.is_empty()); + while let Some(obligation) = self.obligations.pop() { + let ambiguous = match obligation { + Obligation::Prove(ref wc) => { + let PositiveSolution { + free_vars, + universes, + solution, + } = self.prove(wc, minimums)?; + + if solution.has_definite() { + if let Some(constrained_subst) = solution.constrained_subst() { + self.apply_solution(free_vars, universes, constrained_subst); + progress = true; + } + } + + solution.is_ambig() + } + Obligation::Refute(ref goal) => { + let answer = self.refute(goal)?; + answer == NegativeSolution::Ambiguous + } + }; + + if ambiguous { + debug!("ambiguous result: {:?}", obligation); + obligations.push(obligation); + } + } + + self.obligations.extend(obligations.drain(..)); + debug!("end of round, {} obligations left", self.obligations.len()); + } + + // At the end of this process, `self.obligations` should have + // all of the ambiguous obligations, and `obligations` should + // be empty. + assert!(obligations.is_empty()); + + if self.obligations.is_empty() { + Ok(Outcome::Complete) + } else { + Ok(Outcome::Incomplete) + } + } + + /// Try to fulfill all pending obligations and build the resulting + /// solution. The returned solution will transform `subst` substitution with + /// the outcome of type inference by updating the replacements it provides. + pub(super) fn solve( + mut self, + subst: Substitution, + minimums: &mut Minimums, + ) -> Fallible { + let outcome = self.fulfill(minimums)?; + + if self.cannot_prove { + return Ok(Solution::Ambig(Guidance::Unknown)); + } + + if outcome.is_complete() { + // No obligations remain, so we have definitively solved our goals, + // and the current inference state is the unique way to solve them. + + let constraints = self.constraints.into_iter().collect(); + let constrained = self + .infer + .canonicalize(&ConstrainedSubst { subst, constraints }); + return Ok(Solution::Unique(constrained.quantified)); + } + + // Otherwise, we have (positive or negative) obligations remaining, but + // haven't proved that it's *impossible* to satisfy out obligations. we + // need to determine how to package up what we learned about type + // inference as an ambiguous solution. + + if subst.is_trivial_within(&mut self.infer) { + // In this case, we didn't learn *anything* definitively. So now, we + // go one last time through the positive obligations, this time + // applying even *tentative* inference suggestions, so that we can + // yield these upwards as our own suggestions. There are no + // particular guarantees about *which* obligaiton we derive + // suggestions from. + + while let Some(obligation) = self.obligations.pop() { + if let Obligation::Prove(goal) = obligation { + let PositiveSolution { + free_vars, + universes, + solution, + } = self.prove(&goal, minimums).unwrap(); + if let Some(constrained_subst) = solution.constrained_subst() { + self.apply_solution(free_vars, universes, constrained_subst); + let subst = self.infer.canonicalize(&subst); + return Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))); + } + } + } + + Ok(Solution::Ambig(Guidance::Unknown)) + } else { + // While we failed to prove the goal, we still learned that + // something had to hold. Here's an example where this happens: + // + // ```rust + // trait Display {} + // trait Debug {} + // struct Foo {} + // struct Bar {} + // struct Baz {} + // + // impl Display for Bar {} + // impl Display for Baz {} + // + // impl Debug for Foo where T: Display {} + // ``` + // + // If we pose the goal `exists { T: Debug }`, we can't say + // for sure what `T` must be (it could be either `Foo` or + // `Foo`, but we *can* say for sure that it must be of the + // form `Foo`. + let subst = self.infer.canonicalize(&subst); + Ok(Solution::Ambig(Guidance::Definite(subst.quantified))) + } + } +} diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs new file mode 100644 index 00000000000..7fbe4c4d815 --- /dev/null +++ b/chalk-solve/src/recursive/mod.rs @@ -0,0 +1,416 @@ +use fallible::*; +use ir::could_match::CouldMatch; +use std::collections::HashMap; +use std::sync::Arc; + +use super::*; + +mod fulfill; +mod search_graph; +mod stack; + +use self::fulfill::Fulfill; +use self::search_graph::{DepthFirstNumber, SearchGraph}; +use self::stack::{Stack, StackDepth}; + +pub(crate) type UCanonicalGoal = UCanonical>; + +/// A Solver is the basic context in which you can propose goals for a given +/// program. **All questions posed to the solver are in canonical, closed form, +/// so that each question is answered with effectively a "clean slate"**. This +/// allows for better caching, and simplifies management of the inference +/// context. +pub(crate) struct Solver { + program: Arc, + stack: Stack, + search_graph: SearchGraph, + + caching_enabled: bool, + + /// The cache contains **fully solved** goals, whose results are + /// not dependent on the stack in anyway. + cache: HashMap>, +} + +/// The `minimums` struct is used while solving to track whether we encountered +/// any cycles in the process. +#[derive(Copy, Clone, Debug)] +struct Minimums { + positive: DepthFirstNumber, +} + +/// An extension trait for merging `Result`s +trait MergeWith { + fn merge_with(self, other: Self, f: F) -> Self + where + F: FnOnce(T, T) -> T; +} + +impl MergeWith for Fallible { + fn merge_with(self: Fallible, other: Fallible, f: F) -> Fallible + where + F: FnOnce(T, T) -> T, + { + match (self, other) { + (Err(_), Ok(v)) | (Ok(v), Err(_)) => Ok(v), + (Ok(v1), Ok(v2)) => Ok(f(v1, v2)), + (Err(_), Err(e)) => Err(e), + } + } +} + +impl Solver { + crate fn new( + program: &Arc, + overflow_depth: usize, + caching_enabled: bool, + ) -> Self { + Solver { + program: program.clone(), + stack: Stack::new(program, overflow_depth), + search_graph: SearchGraph::new(), + cache: HashMap::new(), + caching_enabled, + } + } + + /// Solves a canonical goal. The substitution returned in the + /// solution will be for the fully decomposed goal. For example, given the + /// program + /// + /// ```ignore + /// struct u8 { } + /// struct SomeType { } + /// trait Foo { } + /// impl Foo for SomeType { } + /// ``` + /// + /// and the goal `exists { forall { SomeType: Foo } + /// }`, `into_peeled_goal` can be used to create a canonical goal + /// `SomeType: Foo`. This function will then return a + /// solution with the substitution `?0 := u8`. + pub(crate) fn solve_root_goal( + &mut self, + canonical_goal: &UCanonical>, + ) -> Fallible { + debug!("solve_root_goal(canonical_goal={:?})", canonical_goal); + assert!(self.stack.is_empty()); + let minimums = &mut Minimums::new(); + self.solve_goal(canonical_goal.clone(), minimums) + } + + /// Attempt to solve a goal that has been fully broken down into leaf form + /// and canonicalized. This is where the action really happens, and is the + /// place where we would perform caching in rustc (and may eventually do in Chalk). + fn solve_goal( + &mut self, + goal: UCanonical>, + minimums: &mut Minimums, + ) -> Fallible { + info_heading!("solve_goal({:?})", goal); + + // First check the cache. + if let Some(value) = self.cache.get(&goal) { + debug!("solve_reduced_goal: cache hit, value={:?}", value); + return value.clone(); + } + + // Next, check if the goal is in the search tree already. + if let Some(dfn) = self.search_graph.lookup(&goal) { + // Check if this table is still on the stack. + if let Some(depth) = self.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? + if self.stack.coinductive_cycle_from(depth) { + let value = ConstrainedSubst { + subst: goal.trivial_substitution(), + constraints: vec![], + }; + debug!("applying coinductive semantics"); + return Ok(Solution::Unique(Canonical { + value, + binders: goal.canonical.binders, + })); + } + + self.stack[depth].flag_cycle(); + } + + minimums.update_from(self.search_graph[dfn].links); + + // Return the solution from the table. + let previous_solution = self.search_graph[dfn].solution.clone(); + debug!( + "solve_goal: cycle detected, previous solution {:?}", + previous_solution + ); + previous_solution + } else { + // Otherwise, push the goal onto the stack and create a table. + // The initial result for this table is error. + let depth = self.stack.push(&goal); + let dfn = self.search_graph.insert(&goal, depth); + let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn); + self.search_graph[dfn].links = subgoal_minimums; + self.search_graph[dfn].stack_depth = None; + self.stack.pop(depth); + minimums.update_from(subgoal_minimums); + + // Read final result from table. + let result = self.search_graph[dfn].solution.clone(); + + // If processing this subgoal did not involve anything + // outside of its subtree, then we can promote it to the + // cache now. This is a sort of hack to alleviate the + // worst of the repeated work that we do during tabling. + if subgoal_minimums.positive >= dfn { + if self.caching_enabled { + debug!("solve_reduced_goal: SCC head encountered, moving to cache"); + self.search_graph.move_to_cache(dfn, &mut self.cache); + } else { + debug!( + "solve_reduced_goal: SCC head encountered, rolling back as caching disabled" + ); + self.search_graph.rollback_to(dfn); + } + } + + debug!("solve_goal: solution = {:?}", result,); + result + } + } + + fn solve_new_subgoal( + &mut self, + canonical_goal: UCanonicalGoal, + depth: StackDepth, + dfn: DepthFirstNumber, + ) -> Minimums { + debug_heading!( + "solve_new_subgoal(canonical_goal={:?}, depth={:?}, dfn={:?})", + canonical_goal, + depth, + dfn, + ); + + // We start with `answer = None` and try to solve the goal. At the end of the iteration, + // `answer` will be updated with the result of the solving process. If we detect a cycle + // during the solving process, we cache `answer` and try to solve the goal again. We repeat + // until we reach a fixed point for `answer`. + // Considering the partial order: + // - None < Some(Unique) < Some(Ambiguous) + // - None < Some(CannotProve) + // the function which maps the loop iteration to `answer` is a nondecreasing function + // so this function will eventually be constant and the loop terminates. + let minimums = &mut Minimums::new(); + loop { + let UCanonical { + universes, + canonical: + Canonical { + binders, + value: InEnvironment { environment, goal }, + }, + } = canonical_goal.clone(); + + let current_answer = match goal { + Goal::Leaf(LeafGoal::DomainGoal(domain_goal)) => { + let canonical_goal = UCanonical { + universes, + canonical: Canonical { + binders, + value: InEnvironment { + environment, + goal: domain_goal, + }, + }, + }; + + // "Domain" goals (i.e., leaf goals that are Rust-specific) are + // always solved via some form of implication. We can either + // apply assumptions from our environment (i.e. where clauses), + // or from the lowered program, which includes fallback + // clauses. We try each approach in turn: + + let InEnvironment { environment, goal } = &canonical_goal.canonical.value; + let env_solution = { + debug_heading!("env_clauses"); + + let env_clauses = environment + .clauses + .iter() + .filter(|&clause| clause.could_match(goal)) + .cloned() + .map(DomainGoal::into_program_clause); + self.solve_from_clauses(&canonical_goal, env_clauses, minimums) + }; + debug!("env_solution={:?}", env_solution); + + let prog_solution = { + debug_heading!("prog_clauses"); + + let prog_clauses: Vec<_> = self + .program + .program_clauses + .iter() + .filter(|&clause| clause.could_match(goal)) + .cloned() + .collect(); + self.solve_from_clauses(&canonical_goal, prog_clauses, minimums) + }; + debug!("prog_solution={:?}", prog_solution); + + // Now that we have all the outcomes, we attempt to combine + // them. Here, we apply a heuristic (also found in rustc): if we + // have possible solutions via both the environment *and* the + // program, we favor the environment; this only impacts type + // inference. The idea is that the assumptions you've explicitly + // made in a given context are more likely to be relevant than + // general `impl`s. + env_solution.merge_with(prog_solution, |env, prog| env.favor_over(prog)) + } + + goal => { + let canonical_goal = UCanonical { + universes, + canonical: Canonical { + binders, + value: InEnvironment { + environment, + goal: goal, + }, + }, + }; + + self.solve_via_simplification(&canonical_goal, minimums) + } + }; + + debug!( + "solve_new_subgoal: loop iteration result = {:?} with minimums {:?}", + current_answer, minimums + ); + + if !self.stack[depth].read_and_reset_cycle_flag() { + // None of our subgoals depended on us directly. + // We can return. + self.search_graph[dfn].solution = current_answer; + return *minimums; + } + + // Some of our subgoals depended on us. We need to re-run + // with the current answer. + if self.search_graph[dfn].solution == current_answer { + // Reached a fixed point. + return *minimums; + } + + let current_answer_is_ambig = match ¤t_answer { + Ok(s) => s.is_ambig(), + Err(_) => false, + }; + + self.search_graph[dfn].solution = current_answer; + + // Subtle: if our current answer is ambiguous, we can just + // stop, and in fact we *must* -- otherwise, wesometimes + // fail to reach a fixed point. See + // `multiple_ambiguous_cycles` for more. + if current_answer_is_ambig { + return *minimums; + } + + // Otherwise: rollback the search tree and try again. + self.search_graph.rollback_to(dfn + 1); + } + } + + fn solve_via_simplification( + &mut self, + canonical_goal: &UCanonical>, + minimums: &mut Minimums, + ) -> Fallible { + debug_heading!("solve_via_simplification({:?})", canonical_goal); + let mut fulfill = Fulfill::new(self); + let (subst, InEnvironment { environment, goal }) = fulfill.initial_subst(canonical_goal); + fulfill.push_goal(&environment, goal)?; + fulfill.solve(subst, minimums) + } + + /// See whether we can solve a goal by implication on any of the given + /// clauses. If multiple such solutions are possible, we attempt to combine + /// them. + fn solve_from_clauses( + &mut self, + canonical_goal: &UCanonical>, + clauses: C, + minimums: &mut Minimums, + ) -> Fallible + where + C: IntoIterator, + { + let mut cur_solution = None; + for ProgramClause { implication, .. } in clauses { + debug_heading!("clause={:?}", implication); + + let res = self.solve_via_implication(canonical_goal, implication, minimums); + if let Ok(solution) = res { + debug!("ok: solution={:?}", solution); + cur_solution = Some(match cur_solution { + None => solution, + Some(cur) => solution.combine(cur), + }); + } else { + debug!("error"); + } + } + cur_solution.ok_or(NoSolution) + } + + /// Modus ponens! That is: try to apply an implication by proving its premises. + fn solve_via_implication( + &mut self, + canonical_goal: &UCanonical>, + clause: Binders, + minimums: &mut Minimums, + ) -> Fallible { + info_heading!( + "solve_via_implication(\ + \n canonical_goal={:?},\ + \n clause={:?})", + canonical_goal, + clause + ); + let mut fulfill = Fulfill::new(self); + let (subst, goal) = fulfill.initial_subst(canonical_goal); + let ProgramClauseImplication { + consequence, + conditions, + } = fulfill.instantiate_binders_existentially(&clause); + + fulfill.unify(&goal.environment, &goal.goal, &consequence)?; + + // if so, toss in all of its premises + for condition in conditions { + fulfill.push_goal(&goal.environment, condition)?; + } + + // and then try to solve + fulfill.solve(subst, minimums) + } +} + +impl Minimums { + fn new() -> Self { + Minimums { + positive: DepthFirstNumber::MAX, + } + } + + fn update_from(&mut self, minimums: Minimums) { + self.positive = ::std::cmp::min(self.positive, minimums.positive); + } +} diff --git a/chalk-solve/src/recursive/search_graph.rs b/chalk-solve/src/recursive/search_graph.rs new file mode 100644 index 00000000000..dd0b87bd90a --- /dev/null +++ b/chalk-solve/src/recursive/search_graph.rs @@ -0,0 +1,127 @@ +use fallible::*; +use solve::Solution; +use std::collections::HashMap; +use std::ops::Add; +use std::ops::Index; +use std::ops::IndexMut; +use std::usize; + +use super::stack::StackDepth; +use super::{Minimums, UCanonicalGoal}; + +pub(super) struct SearchGraph { + indices: HashMap, + nodes: Vec, +} + +#[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)] +pub(super) struct DepthFirstNumber { + index: usize, +} + +pub(super) struct Node { + pub(crate) goal: UCanonicalGoal, + + pub(crate) solution: Fallible, + + /// This is `Some(X)` if we are actively exploring this node, or + /// `None` otherwise. + pub(crate) stack_depth: Option, + + /// While this node is on the stack, this field will be set to + /// contain our own depth-first number. Once the node is popped + /// 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, +} + +impl SearchGraph { + pub(crate) fn new() -> Self { + SearchGraph { + indices: HashMap::new(), + nodes: vec![], + } + } + + pub(crate) fn lookup(&self, goal: &UCanonicalGoal) -> Option { + self.indices.get(goal).cloned() + } + + /// Insert a new search node in the tree. The node will be in the initial + /// state for a search node: + /// + /// - stack depth as given + /// - links set to its own DFN + /// - solution is initially `NoSolution` + pub(crate) fn insert( + &mut self, + goal: &UCanonicalGoal, + stack_depth: StackDepth, + ) -> DepthFirstNumber { + let dfn = DepthFirstNumber { + index: self.nodes.len(), + }; + let node = Node { + goal: goal.clone(), + solution: Err(NoSolution), + stack_depth: Some(stack_depth), + links: Minimums { positive: dfn }, + }; + self.nodes.push(node); + let previous_index = self.indices.insert(goal.clone(), dfn); + assert!(previous_index.is_none()); + dfn + } + + /// Clears all nodes with a depth-first number greater than or equal `dfn`. + pub(crate) fn rollback_to(&mut self, dfn: DepthFirstNumber) { + debug!("rollback_to(dfn={:?})", dfn); + self.indices.retain(|_key, value| *value < dfn); + self.nodes.truncate(dfn.index); + } + + /// Removes all nodes with a depth-first-number greater than or + /// equal to `dfn`, adding their final solutions into the cache. + pub(crate) fn move_to_cache( + &mut self, + dfn: DepthFirstNumber, + cache: &mut HashMap>, + ) { + debug!("move_to_cache(dfn={:?})", dfn); + self.indices.retain(|_key, value| *value < dfn); + for node in self.nodes.drain(dfn.index..) { + assert!(node.stack_depth.is_none()); + assert!(node.links.positive >= dfn); + debug!("caching solution {:?} for {:?}", node.solution, node.goal); + cache.insert(node.goal, node.solution); + } + } +} + +impl Index for SearchGraph { + type Output = Node; + + fn index(&self, table_index: DepthFirstNumber) -> &Node { + &self.nodes[table_index.index] + } +} + +impl IndexMut for SearchGraph { + fn index_mut(&mut self, table_index: DepthFirstNumber) -> &mut Node { + &mut self.nodes[table_index.index] + } +} + +impl DepthFirstNumber { + pub(crate) const MAX: DepthFirstNumber = DepthFirstNumber { index: usize::MAX }; +} + +impl Add for DepthFirstNumber { + type Output = DepthFirstNumber; + + fn add(self, v: usize) -> DepthFirstNumber { + DepthFirstNumber { + index: self.index + v, + } + } +} diff --git a/chalk-solve/src/recursive/stack.rs b/chalk-solve/src/recursive/stack.rs new file mode 100644 index 00000000000..9a4a8e8909a --- /dev/null +++ b/chalk-solve/src/recursive/stack.rs @@ -0,0 +1,103 @@ +use ir::ProgramEnvironment; +use std::mem; +use std::ops::Index; +use std::ops::IndexMut; +use std::sync::Arc; +use std::usize; + +use super::UCanonicalGoal; + +pub(crate) struct Stack { + program: Arc, + entries: Vec, + overflow_depth: usize, +} + +#[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)] +pub(crate) struct StackDepth { + depth: usize, +} + +/// The data we actively keep for each goal on the stack. +pub(crate) struct StackEntry { + /// Was this a coinductive goal? + coinductive_goal: bool, + + /// Initially false, set to true when some subgoal depends on us. + cycle: bool, +} + +impl Stack { + pub(crate) fn new(program: &Arc, overflow_depth: usize) -> Self { + Stack { + program: program.clone(), + entries: vec![], + overflow_depth: overflow_depth, + } + } + + pub(crate) fn is_empty(&self) -> bool { + self.entries.is_empty() + } + + pub(crate) fn push(&mut self, goal: &UCanonicalGoal) -> StackDepth { + let depth = StackDepth { + depth: self.entries.len(), + }; + + if depth.depth >= self.overflow_depth { + // This shoudl perhaps be a result or something, though + // really I'd prefer to move to subgoal abstraction for + // guaranteeing termination. -nmatsakis + panic!("overflow depth reached") + } + + let coinductive_goal = goal.is_coinductive(&self.program); + self.entries.push(StackEntry { + coinductive_goal, + cycle: false, + }); + depth + } + + pub(crate) fn pop(&mut self, depth: StackDepth) { + assert_eq!( + depth.depth + 1, + self.entries.len(), + "mismatched stack push/pop" + ); + self.entries.pop(); + } + + /// True if all the goals from the top of the stack down to (and + /// including) the given depth are coinductive. + pub(crate) fn coinductive_cycle_from(&self, depth: StackDepth) -> bool { + self.entries[depth.depth..] + .iter() + .all(|entry| entry.coinductive_goal) + } +} + +impl StackEntry { + pub(crate) fn flag_cycle(&mut self) { + self.cycle = true; + } + + pub(crate) fn read_and_reset_cycle_flag(&mut self) -> bool { + mem::replace(&mut self.cycle, false) + } +} + +impl Index for Stack { + type Output = StackEntry; + + fn index(&self, depth: StackDepth) -> &StackEntry { + &self.entries[depth.depth] + } +} + +impl IndexMut for Stack { + fn index_mut(&mut self, depth: StackDepth) -> &mut StackEntry { + &mut self.entries[depth.depth] + } +} diff --git a/chalk-solve/src/recursive/tables.rs b/chalk-solve/src/recursive/tables.rs new file mode 100644 index 00000000000..379078db446 --- /dev/null +++ b/chalk-solve/src/recursive/tables.rs @@ -0,0 +1,57 @@ +use fallible::*; +use std::ops::Index; +use std::ops::IndexMut; + +use super::stack::StackDepth; + +#[derive(Default)] +pub(crate) struct Tables { + indices: HashMap, + tables: Vec, +} + +pub(crate) struct TableIndex { + index: usize, +} + +pub(crate) struct Table { + crate solution: Fallible, + crate stack_depth: Option, +} + +impl Tables { + pub(crate) fn lookup(&self, goal: &CanonicalLeafGoal) -> Option { + self.indices.get(goal) + } + + pub(crate) fn insert( + &mut self, + goal: &CanonicalLeafGoal, + solution: Fallible, + stack_depth: Option, + ) -> TableIndex { + let table = Table { + solution, + stack_depth, + }; + let index = self.tables.len(); + self.tables.push(table); + let previous_index = self.indices.insert(goal.clone(), index); + assert!(previous_index.is_none()); + TableIndex { index } + } +} + +impl Index for Tables { + type Output = Table; + + fn index(&self, table_index: TableIndex) -> &Table { + &self.tables[table_index.index] + } +} + +impl IndexMut for Tables { + fn index(&self, table_index: TableIndex) -> &mut Table { + &self.tables[table_index.index] + } +} From 9bb94d191cdae79632145a3225804f746b10b040 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 13:43:35 +0100 Subject: [PATCH 02/50] Getting past name resolution errors --- chalk-solve/src/recursive/fulfill.rs | 89 ++++++++++++---------- chalk-solve/src/recursive/mod.rs | 93 +++++++++++------------ chalk-solve/src/recursive/search_graph.rs | 35 ++++----- chalk-solve/src/recursive/stack.rs | 19 ++--- chalk-solve/src/recursive/tables.rs | 6 +- 5 files changed, 125 insertions(+), 117 deletions(-) diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index c3c504819f2..c82ebab5571 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -1,13 +1,15 @@ use super::*; use cast::Caster; +use chalk_engine::fallible::NoSolution; use fold::Fold; -use solve::infer::{ +use infer::{ canonicalize::Canonicalized, - instantiate::BindersAndValue, + instantiate::IntoBindersAndValue, ucanonicalize::{UCanonicalized, UniverseMap}, unify::UnificationResult, - InferenceTable, ParameterInferenceVariable, + InferenceTable, }; +use interner::HasInterner; use std::collections::HashSet; use std::fmt::Debug; use std::sync::Arc; @@ -29,24 +31,24 @@ impl Outcome { /// A goal that must be resolved #[derive(Clone, Debug, PartialEq, Eq)] -enum Obligation { +enum Obligation { /// For "positive" goals, we flatten all the way out to leafs within the /// current `Fulfill` - Prove(InEnvironment), + Prove(InEnvironment>), /// For "negative" goals, we don't flatten in *this* `Fulfill`, which would /// require having a logical "or" operator. Instead, we recursively solve in /// a fresh `Fulfill`. - Refute(InEnvironment), + Refute(InEnvironment>), } /// When proving a leaf goal, we record the free variables that appear within it /// so that we can update inference state accordingly. #[derive(Clone, Debug)] -struct PositiveSolution { - free_vars: Vec, +struct PositiveSolution { + free_vars: Vec, universes: UniverseMap, - solution: Solution, + solution: Solution, } /// When refuting a goal, there's no impact on inference state. @@ -66,16 +68,16 @@ enum NegativeSolution { /// of type inference in general. But when solving trait constraints, *fresh* /// `Fulfill` instances will be created to solve canonicalized, free-standing /// goals, and transport what was learned back to the outer context. -crate struct Fulfill<'s> { - solver: &'s mut Solver, - infer: InferenceTable, +pub(crate) struct Fulfill<'s, I: Interner> { + solver: &'s mut Solver, + infer: InferenceTable, /// The remaining goals to prove or refute - obligations: Vec, + obligations: Vec>, /// Lifetime constraints that must be fulfilled for a solution to be fully /// validated. - constraints: HashSet>, + constraints: HashSet>>, /// Record that a goal has been processed that can neither be proved nor /// refuted. In such a case the solution will be either `CannotProve`, or `Err` @@ -83,8 +85,8 @@ crate struct Fulfill<'s> { cannot_prove: bool, } -impl<'s> Fulfill<'s> { - pub(crate) fn new(solver: &'s mut Solver) -> Self { +impl<'s, I: Interner> Fulfill<'s, I> { + pub(crate) fn new(solver: &'s mut Solver) -> Self { Fulfill { solver, infer: InferenceTable::new(), @@ -100,10 +102,10 @@ impl<'s> Fulfill<'s> { /// then later be used as the answer to be returned to the user. /// /// See also `InferenceTable::fresh_subst`. - pub(crate) fn initial_subst>( + pub(crate) fn initial_subst + HasInterner>( &mut self, ucanonical_goal: &UCanonical>, - ) -> (Substitution, InEnvironment) { + ) -> (Substitution, InEnvironment) { let canonical_goal = self.infer.instantiate_universes(ucanonical_goal); let subst = self.infer.fresh_subst(&canonical_goal.binders); let value = canonical_goal.substitute(&subst); @@ -114,10 +116,10 @@ impl<'s> Fulfill<'s> { #[allow(non_camel_case_types)] pub(crate) fn instantiate_binders_existentially( &mut self, - arg: &impl BindersAndValue, + arg: &impl IntoBindersAndValue, ) -> T::Result where - T: Fold, + T: Fold, { self.infer.instantiate_binders_existentially(arg) } @@ -126,9 +128,14 @@ impl<'s> Fulfill<'s> { /// /// Wraps `InferenceTable::unify`; any resulting normalizations are added /// into our list of pending obligations with the given environment. - pub(crate) fn unify(&mut self, environment: &Arc, a: &T, b: &T) -> Fallible<()> + pub(crate) fn unify( + &mut self, + environment: &Arc>, + a: &T, + b: &T, + ) -> Fallible<()> where - T: ?Sized + Zip + Debug, + T: ?Sized + Zip + Debug, { let UnificationResult { goals, constraints } = self.infer.unify(environment, a, b)?; debug!("unify({:?}, {:?}) succeeded", a, b); @@ -142,37 +149,41 @@ impl<'s> Fulfill<'s> { /// Create obligations for the given goal in the given environment. This may /// ultimately create any number of obligations. - pub(crate) fn push_goal(&mut self, environment: &Arc, goal: Goal) -> Fallible<()> { + pub(crate) fn push_goal( + &mut self, + environment: &Arc>, + goal: Goal, + ) -> Fallible<()> { debug!("push_goal({:?}, {:?})", goal, environment); - match goal { - Goal::Quantified(QuantifierKind::ForAll, subgoal) => { + match goal.data() { + GoalData::Quantified(QuantifierKind::ForAll, subgoal) => { let subgoal = self.infer.instantiate_binders_universally(&subgoal); self.push_goal(environment, *subgoal)?; } - Goal::Quantified(QuantifierKind::Exists, subgoal) => { + GoalData::Quantified(QuantifierKind::Exists, subgoal) => { let subgoal = self.infer.instantiate_binders_existentially(&subgoal); self.push_goal(environment, *subgoal)?; } - Goal::Implies(wc, subgoal) => { + GoalData::Implies(wc, subgoal) => { let new_environment = &environment.add_clauses(wc); self.push_goal(new_environment, *subgoal)?; } - Goal::And(subgoal1, subgoal2) => { + GoalData::And(subgoal1, subgoal2) => { self.push_goal(environment, *subgoal1)?; self.push_goal(environment, *subgoal2)?; } - Goal::Not(subgoal) => { + GoalData::Not(subgoal) => { let in_env = InEnvironment::new(environment, *subgoal); self.obligations.push(Obligation::Refute(in_env)); } - Goal::Leaf(LeafGoal::DomainGoal(_)) => { + GoalData::DomainGoal(_) => { let in_env = InEnvironment::new(environment, goal); self.obligations.push(Obligation::Prove(in_env)); } - Goal::Leaf(LeafGoal::EqGoal(EqGoal { a, b })) => { + GoalData::EqGoal(EqGoal { a, b }) => { self.unify(&environment, &a, &b)?; } - Goal::CannotProve(()) => { + GoalData::CannotProve(()) => { self.cannot_prove = true; } } @@ -181,9 +192,9 @@ impl<'s> Fulfill<'s> { fn prove( &mut self, - wc: &InEnvironment, + wc: &InEnvironment>, minimums: &mut Minimums, - ) -> Fallible { + ) -> Fallible> { let Canonicalized { quantified, free_vars, @@ -200,7 +211,7 @@ impl<'s> Fulfill<'s> { }) } - fn refute(&mut self, goal: &InEnvironment) -> Fallible { + fn refute(&mut self, goal: &InEnvironment>) -> Fallible { let canonicalized = match self.infer.invert_then_canonicalize(goal) { Some(v) => v, None => { @@ -237,9 +248,9 @@ impl<'s> Fulfill<'s> { /// be mapped into our variables with `free_vars`. fn apply_solution( &mut self, - free_vars: Vec, + free_vars: Vec, universes: UniverseMap, - subst: Canonical, + subst: Canonical>, ) { let subst = universes.map_from_canonical(&subst); let ConstrainedSubst { subst, constraints } = self.infer.instantiate_canonical(&subst); @@ -341,9 +352,9 @@ impl<'s> Fulfill<'s> { /// the outcome of type inference by updating the replacements it provides. pub(super) fn solve( mut self, - subst: Substitution, + subst: Substitution, minimums: &mut Minimums, - ) -> Fallible { + ) -> Fallible> { let outcome = self.fulfill(minimums)?; if self.cannot_prove { diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 7fbe4c4d815..b486a8f36b5 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -1,8 +1,3 @@ -use fallible::*; -use ir::could_match::CouldMatch; -use std::collections::HashMap; -use std::sync::Arc; - use super::*; mod fulfill; @@ -12,24 +7,21 @@ mod stack; use self::fulfill::Fulfill; use self::search_graph::{DepthFirstNumber, SearchGraph}; use self::stack::{Stack, StackDepth}; +use chalk_engine::fallible::{Fallible, NoSolution}; -pub(crate) type UCanonicalGoal = UCanonical>; +type UCanonicalGoal = UCanonical>>; /// A Solver is the basic context in which you can propose goals for a given /// program. **All questions posed to the solver are in canonical, closed form, /// so that each question is answered with effectively a "clean slate"**. This /// allows for better caching, and simplifies management of the inference /// context. -pub(crate) struct Solver { - program: Arc, +pub(crate) struct Solver { + // program: &dyn RustIrDatabase, stack: Stack, - search_graph: SearchGraph, + search_graph: SearchGraph, caching_enabled: bool, - - /// The cache contains **fully solved** goals, whose results are - /// not dependent on the stack in anyway. - cache: HashMap>, } /// The `minimums` struct is used while solving to track whether we encountered @@ -59,17 +51,16 @@ impl MergeWith for Fallible { } } -impl Solver { - crate fn new( - program: &Arc, +impl Solver { + pub(crate) fn new( + // program: &Arc, overflow_depth: usize, caching_enabled: bool, ) -> Self { Solver { - program: program.clone(), - stack: Stack::new(program, overflow_depth), + // program: program.clone(), + stack: Stack::new(overflow_depth), search_graph: SearchGraph::new(), - cache: HashMap::new(), caching_enabled, } } @@ -91,8 +82,8 @@ impl Solver { /// solution with the substitution `?0 := u8`. pub(crate) fn solve_root_goal( &mut self, - canonical_goal: &UCanonical>, - ) -> Fallible { + canonical_goal: &UCanonicalGoal, + ) -> Fallible> { debug!("solve_root_goal(canonical_goal={:?})", canonical_goal); assert!(self.stack.is_empty()); let minimums = &mut Minimums::new(); @@ -104,9 +95,9 @@ impl Solver { /// place where we would perform caching in rustc (and may eventually do in Chalk). fn solve_goal( &mut self, - goal: UCanonical>, + goal: UCanonicalGoal, minimums: &mut Minimums, - ) -> Fallible { + ) -> Fallible> { info_heading!("solve_goal({:?})", goal); // First check the cache. @@ -185,7 +176,7 @@ impl Solver { fn solve_new_subgoal( &mut self, - canonical_goal: UCanonicalGoal, + canonical_goal: UCanonicalGoal, depth: StackDepth, dfn: DepthFirstNumber, ) -> Minimums { @@ -216,8 +207,8 @@ impl Solver { }, } = canonical_goal.clone(); - let current_answer = match goal { - Goal::Leaf(LeafGoal::DomainGoal(domain_goal)) => { + let current_answer = match goal.data() { + GoalData::DomainGoal(domain_goal) => { let canonical_goal = UCanonical { universes, canonical: Canonical { @@ -278,10 +269,7 @@ impl Solver { universes, canonical: Canonical { binders, - value: InEnvironment { - environment, - goal: goal, - }, + value: InEnvironment { environment, goal }, }, }; @@ -330,9 +318,9 @@ impl Solver { fn solve_via_simplification( &mut self, - canonical_goal: &UCanonical>, + canonical_goal: &UCanonicalGoal, minimums: &mut Minimums, - ) -> Fallible { + ) -> Fallible> { debug_heading!("solve_via_simplification({:?})", canonical_goal); let mut fulfill = Fulfill::new(self); let (subst, InEnvironment { environment, goal }) = fulfill.initial_subst(canonical_goal); @@ -345,26 +333,31 @@ impl Solver { /// them. fn solve_from_clauses( &mut self, - canonical_goal: &UCanonical>, + canonical_goal: &UCanonical>>, clauses: C, minimums: &mut Minimums, - ) -> Fallible + ) -> Fallible> where - C: IntoIterator, + C: IntoIterator>, { let mut cur_solution = None; - for ProgramClause { implication, .. } in clauses { - debug_heading!("clause={:?}", implication); - - let res = self.solve_via_implication(canonical_goal, implication, minimums); - if let Ok(solution) = res { - debug!("ok: solution={:?}", solution); - cur_solution = Some(match cur_solution { - None => solution, - Some(cur) => solution.combine(cur), - }); - } else { - debug!("error"); + for program_clause in clauses { + debug_heading!("clause={:?}", program_clause); + + match program_clause { + ProgramClause::Implies(implication) => { + let res = self.solve_via_implication(canonical_goal, implication, minimums); + if let Ok(solution) = res { + debug!("ok: solution={:?}", solution); + cur_solution = Some(match cur_solution { + None => solution, + Some(cur) => solution.combine(cur), + }); + } else { + debug!("error"); + } + } + ProgramClause::ForAll(_) => todo!(), } } cur_solution.ok_or(NoSolution) @@ -373,10 +366,10 @@ impl Solver { /// Modus ponens! That is: try to apply an implication by proving its premises. fn solve_via_implication( &mut self, - canonical_goal: &UCanonical>, - clause: Binders, + canonical_goal: &UCanonical>>, + clause: Binders>, minimums: &mut Minimums, - ) -> Fallible { + ) -> Fallible> { info_heading!( "solve_via_implication(\ \n canonical_goal={:?},\ diff --git a/chalk-solve/src/recursive/search_graph.rs b/chalk-solve/src/recursive/search_graph.rs index dd0b87bd90a..26f17ca3ac2 100644 --- a/chalk-solve/src/recursive/search_graph.rs +++ b/chalk-solve/src/recursive/search_graph.rs @@ -1,5 +1,3 @@ -use fallible::*; -use solve::Solution; use std::collections::HashMap; use std::ops::Add; use std::ops::Index; @@ -8,10 +6,13 @@ use std::usize; use super::stack::StackDepth; use super::{Minimums, UCanonicalGoal}; +use crate::Solution; +use chalk_engine::fallible::{Fallible, NoSolution}; +use chalk_ir::interner::Interner; -pub(super) struct SearchGraph { - indices: HashMap, - nodes: Vec, +pub(super) struct SearchGraph { + indices: HashMap, DepthFirstNumber>, + nodes: Vec>, } #[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)] @@ -19,10 +20,10 @@ pub(super) struct DepthFirstNumber { index: usize, } -pub(super) struct Node { - pub(crate) goal: UCanonicalGoal, +pub(super) struct Node { + pub(crate) goal: UCanonicalGoal, - pub(crate) solution: Fallible, + pub(crate) solution: Fallible>, /// This is `Some(X)` if we are actively exploring this node, or /// `None` otherwise. @@ -35,7 +36,7 @@ pub(super) struct Node { pub(crate) links: Minimums, } -impl SearchGraph { +impl SearchGraph { pub(crate) fn new() -> Self { SearchGraph { indices: HashMap::new(), @@ -43,7 +44,7 @@ impl SearchGraph { } } - pub(crate) fn lookup(&self, goal: &UCanonicalGoal) -> Option { + pub(crate) fn lookup(&self, goal: &UCanonicalGoal) -> Option { self.indices.get(goal).cloned() } @@ -55,7 +56,7 @@ impl SearchGraph { /// - solution is initially `NoSolution` pub(crate) fn insert( &mut self, - goal: &UCanonicalGoal, + goal: &UCanonicalGoal, stack_depth: StackDepth, ) -> DepthFirstNumber { let dfn = DepthFirstNumber { @@ -85,7 +86,7 @@ impl SearchGraph { pub(crate) fn move_to_cache( &mut self, dfn: DepthFirstNumber, - cache: &mut HashMap>, + cache: &mut HashMap, Fallible>>, ) { debug!("move_to_cache(dfn={:?})", dfn); self.indices.retain(|_key, value| *value < dfn); @@ -98,16 +99,16 @@ impl SearchGraph { } } -impl Index for SearchGraph { - type Output = Node; +impl Index for SearchGraph { + type Output = Node; - fn index(&self, table_index: DepthFirstNumber) -> &Node { + fn index(&self, table_index: DepthFirstNumber) -> &Node { &self.nodes[table_index.index] } } -impl IndexMut for SearchGraph { - fn index_mut(&mut self, table_index: DepthFirstNumber) -> &mut Node { +impl IndexMut for SearchGraph { + fn index_mut(&mut self, table_index: DepthFirstNumber) -> &mut Node { &mut self.nodes[table_index.index] } } diff --git a/chalk-solve/src/recursive/stack.rs b/chalk-solve/src/recursive/stack.rs index 9a4a8e8909a..7d21fea4f72 100644 --- a/chalk-solve/src/recursive/stack.rs +++ b/chalk-solve/src/recursive/stack.rs @@ -1,14 +1,12 @@ -use ir::ProgramEnvironment; +use super::UCanonicalGoal; +use chalk_ir::interner::Interner; use std::mem; use std::ops::Index; use std::ops::IndexMut; -use std::sync::Arc; use std::usize; -use super::UCanonicalGoal; - pub(crate) struct Stack { - program: Arc, + // program: Arc, entries: Vec, overflow_depth: usize, } @@ -28,11 +26,14 @@ pub(crate) struct StackEntry { } impl Stack { - pub(crate) fn new(program: &Arc, overflow_depth: usize) -> Self { + pub(crate) fn new( + // program: &Arc, + overflow_depth: usize, + ) -> Self { Stack { - program: program.clone(), + // program: program.clone(), entries: vec![], - overflow_depth: overflow_depth, + overflow_depth, } } @@ -40,7 +41,7 @@ impl Stack { self.entries.is_empty() } - pub(crate) fn push(&mut self, goal: &UCanonicalGoal) -> StackDepth { + pub(crate) fn push(&mut self, goal: &UCanonicalGoal) -> StackDepth { let depth = StackDepth { depth: self.entries.len(), }; diff --git a/chalk-solve/src/recursive/tables.rs b/chalk-solve/src/recursive/tables.rs index 379078db446..42e27755603 100644 --- a/chalk-solve/src/recursive/tables.rs +++ b/chalk-solve/src/recursive/tables.rs @@ -4,6 +4,8 @@ use std::ops::IndexMut; use super::stack::StackDepth; +// TODO this file doesn't seem used + #[derive(Default)] pub(crate) struct Tables { indices: HashMap, @@ -15,8 +17,8 @@ pub(crate) struct TableIndex { } pub(crate) struct Table { - crate solution: Fallible, - crate stack_depth: Option, + pub(crate) solution: Fallible, + pub(crate) stack_depth: Option, } impl Tables { From 6fc0808b20d9865d1aec3fcc0d28561c61ef0796 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 14:19:51 +0100 Subject: [PATCH 03/50] Fix many errors --- chalk-solve/src/recursive/fulfill.rs | 68 +++++++++++++++++----------- chalk-solve/src/recursive/mod.rs | 56 +++++++++++++++-------- 2 files changed, 79 insertions(+), 45 deletions(-) diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index c82ebab5571..81ada121d95 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -7,7 +7,7 @@ use infer::{ instantiate::IntoBindersAndValue, ucanonicalize::{UCanonicalized, UniverseMap}, unify::UnificationResult, - InferenceTable, + InferenceTable, ParameterEnaVariable, ParameterEnaVariableExt, }; use interner::HasInterner; use std::collections::HashSet; @@ -46,7 +46,7 @@ enum Obligation { /// so that we can update inference state accordingly. #[derive(Clone, Debug)] struct PositiveSolution { - free_vars: Vec, + free_vars: Vec>, universes: UniverseMap, solution: Solution, } @@ -69,7 +69,7 @@ enum NegativeSolution { /// `Fulfill` instances will be created to solve canonicalized, free-standing /// goals, and transport what was learned back to the outer context. pub(crate) struct Fulfill<'s, I: Interner> { - solver: &'s mut Solver, + solver: &'s mut Solver<'s, I>, infer: InferenceTable, /// The remaining goals to prove or refute @@ -86,7 +86,7 @@ pub(crate) struct Fulfill<'s, I: Interner> { } impl<'s, I: Interner> Fulfill<'s, I> { - pub(crate) fn new(solver: &'s mut Solver) -> Self { + pub(crate) fn new(solver: &'s mut Solver<'s, I>) -> Self { Fulfill { solver, infer: InferenceTable::new(), @@ -107,7 +107,9 @@ impl<'s, I: Interner> Fulfill<'s, I> { ucanonical_goal: &UCanonical>, ) -> (Substitution, InEnvironment) { let canonical_goal = self.infer.instantiate_universes(ucanonical_goal); - let subst = self.infer.fresh_subst(&canonical_goal.binders); + let subst = self + .infer + .fresh_subst(self.solver.program.interner(), &canonical_goal.binders); let value = canonical_goal.substitute(&subst); (subst, value) } @@ -116,12 +118,13 @@ impl<'s, I: Interner> Fulfill<'s, I> { #[allow(non_camel_case_types)] pub(crate) fn instantiate_binders_existentially( &mut self, - arg: &impl IntoBindersAndValue, + arg: impl IntoBindersAndValue, ) -> T::Result where T: Fold, { - self.infer.instantiate_binders_existentially(arg) + self.infer + .instantiate_binders_existentially(self.solver.program.interner(), arg) } /// Unifies `a` and `b` in the given environment. @@ -137,7 +140,8 @@ impl<'s, I: Interner> Fulfill<'s, I> { where T: ?Sized + Zip + Debug, { - let UnificationResult { goals, constraints } = self.infer.unify(environment, a, b)?; + let UnificationResult { goals, constraints } = + self.infer.unify(self.interner(), environment, a, b)?; debug!("unify({:?}, {:?}) succeeded", a, b); debug!("unify: goals={:?}", goals); debug!("unify: constraints={:?}", constraints); @@ -157,20 +161,25 @@ impl<'s, I: Interner> Fulfill<'s, I> { debug!("push_goal({:?}, {:?})", goal, environment); match goal.data() { GoalData::Quantified(QuantifierKind::ForAll, subgoal) => { - let subgoal = self.infer.instantiate_binders_universally(&subgoal); - self.push_goal(environment, *subgoal)?; + let subgoal = self + .infer + .instantiate_binders_universally(self.interner(), subgoal); + self.push_goal(environment, subgoal)?; } GoalData::Quantified(QuantifierKind::Exists, subgoal) => { - let subgoal = self.infer.instantiate_binders_existentially(&subgoal); - self.push_goal(environment, *subgoal)?; + let subgoal = self + .infer + .instantiate_binders_existentially(self.interner(), subgoal); + self.push_goal(environment, subgoal)?; } GoalData::Implies(wc, subgoal) => { - let new_environment = &environment.add_clauses(wc); + let new_environment = &environment.add_clauses(wc.iter().cloned()); self.push_goal(new_environment, *subgoal)?; } - GoalData::And(subgoal1, subgoal2) => { - self.push_goal(environment, *subgoal1)?; - self.push_goal(environment, *subgoal2)?; + GoalData::All(goals) => { + for subgoal in goals.as_slice() { + self.push_goal(environment, subgoal.clone())?; + } } GoalData::Not(subgoal) => { let in_env = InEnvironment::new(environment, *subgoal); @@ -199,11 +208,11 @@ impl<'s, I: Interner> Fulfill<'s, I> { quantified, free_vars, max_universe: _, - } = self.infer.canonicalize(wc); + } = self.infer.canonicalize(self.interner(), wc); let UCanonicalized { quantified, universes, - } = self.infer.u_canonicalize(&quantified); + } = self.infer.u_canonicalize(self.interner(), &quantified); Ok(PositiveSolution { free_vars, universes, @@ -225,7 +234,7 @@ impl<'s, I: Interner> Fulfill<'s, I> { let UCanonicalized { quantified, universes: _, - } = self.infer.u_canonicalize(&canonicalized); + } = self.infer.u_canonicalize(self.interner(), &canonicalized); let mut minimums = Minimums::new(); // FIXME -- minimums here seems wrong if let Ok(solution) = self.solver.solve_goal(quantified, &mut minimums) { if solution.is_unique() { @@ -248,12 +257,13 @@ impl<'s, I: Interner> Fulfill<'s, I> { /// be mapped into our variables with `free_vars`. fn apply_solution( &mut self, - free_vars: Vec, + free_vars: Vec>, universes: UniverseMap, subst: Canonical>, ) { - let subst = universes.map_from_canonical(&subst); - let ConstrainedSubst { subst, constraints } = self.infer.instantiate_canonical(&subst); + let subst = universes.map_from_canonical(self.interner(), &subst); + let ConstrainedSubst { subst, constraints } = + self.infer.instantiate_canonical(self.interner(), &subst); debug!( "fulfill::apply_solution: adding constraints {:?}", @@ -267,8 +277,8 @@ impl<'s, I: Interner> Fulfill<'s, I> { let empty_env = &Environment::new(); for (i, free_var) in free_vars.into_iter().enumerate() { - let subst_value = &subst.parameters[i]; - let free_value = free_var.to_parameter(); + let subst_value = subst.at(i); + let free_value = free_var.to_parameter(self.interner()); self.unify(empty_env, &free_value, subst_value) .unwrap_or_else(|err| { panic!( @@ -368,7 +378,7 @@ impl<'s, I: Interner> Fulfill<'s, I> { let constraints = self.constraints.into_iter().collect(); let constrained = self .infer - .canonicalize(&ConstrainedSubst { subst, constraints }); + .canonicalize(self.interner(), &ConstrainedSubst { subst, constraints }); return Ok(Solution::Unique(constrained.quantified)); } @@ -394,7 +404,7 @@ impl<'s, I: Interner> Fulfill<'s, I> { } = self.prove(&goal, minimums).unwrap(); if let Some(constrained_subst) = solution.constrained_subst() { self.apply_solution(free_vars, universes, constrained_subst); - let subst = self.infer.canonicalize(&subst); + let subst = self.infer.canonicalize(self.interner(), &subst); return Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))); } } @@ -422,8 +432,12 @@ impl<'s, I: Interner> Fulfill<'s, I> { // for sure what `T` must be (it could be either `Foo` or // `Foo`, but we *can* say for sure that it must be of the // form `Foo`. - let subst = self.infer.canonicalize(&subst); + let subst = self.infer.canonicalize(self.interner(), &subst); Ok(Solution::Ambig(Guidance::Definite(subst.quantified))) } } + + fn interner(&self) -> &I { + self.solver.program.interner() + } } diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index b486a8f36b5..7535cac891a 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -8,6 +8,7 @@ use self::fulfill::Fulfill; use self::search_graph::{DepthFirstNumber, SearchGraph}; use self::stack::{Stack, StackDepth}; use chalk_engine::fallible::{Fallible, NoSolution}; +use chalk_ir::could_match::CouldMatch; type UCanonicalGoal = UCanonical>>; @@ -16,8 +17,8 @@ type UCanonicalGoal = UCanonical>>; /// so that each question is answered with effectively a "clean slate"**. This /// allows for better caching, and simplifies management of the inference /// context. -pub(crate) struct Solver { - // program: &dyn RustIrDatabase, +pub(crate) struct Solver<'me, I: Interner> { + program: &'me dyn RustIrDatabase, stack: Stack, search_graph: SearchGraph, @@ -51,14 +52,14 @@ impl MergeWith for Fallible { } } -impl Solver { +impl<'me, I: Interner> Solver<'me, I> { pub(crate) fn new( - // program: &Arc, + program: &'me dyn RustIrDatabase, overflow_depth: usize, caching_enabled: bool, ) -> Self { Solver { - // program: program.clone(), + program, stack: Stack::new(overflow_depth), search_graph: SearchGraph::new(), caching_enabled, @@ -101,10 +102,11 @@ impl Solver { info_heading!("solve_goal({:?})", goal); // First check the cache. - if let Some(value) = self.cache.get(&goal) { - debug!("solve_reduced_goal: cache hit, value={:?}", value); - return value.clone(); - } + // TODO + // if let Some(value) = self.cache.get(&goal) { + // debug!("solve_reduced_goal: cache hit, value={:?}", value); + // return value.clone(); + // } // Next, check if the goal is in the search tree already. if let Some(dfn) = self.search_graph.lookup(&goal) { @@ -159,8 +161,9 @@ impl Solver { // worst of the repeated work that we do during tabling. if subgoal_minimums.positive >= dfn { if self.caching_enabled { + // TODO + // self.search_graph.move_to_cache(dfn, &mut self.cache); debug!("solve_reduced_goal: SCC head encountered, moving to cache"); - self.search_graph.move_to_cache(dfn, &mut self.cache); } else { debug!( "solve_reduced_goal: SCC head encountered, rolling back as caching disabled" @@ -215,7 +218,7 @@ impl Solver { binders, value: InEnvironment { environment, - goal: domain_goal, + goal: domain_goal.clone(), }, }, }; @@ -234,8 +237,7 @@ impl Solver { .clauses .iter() .filter(|&clause| clause.could_match(goal)) - .cloned() - .map(DomainGoal::into_program_clause); + .cloned(); self.solve_from_clauses(&canonical_goal, env_clauses, minimums) }; debug!("env_solution={:?}", env_solution); @@ -264,7 +266,7 @@ impl Solver { env_solution.merge_with(prog_solution, |env, prog| env.favor_over(prog)) } - goal => { + _ => { let canonical_goal = UCanonical { universes, canonical: Canonical { @@ -297,7 +299,7 @@ impl Solver { } let current_answer_is_ambig = match ¤t_answer { - Ok(s) => s.is_ambig(), + Ok(s) => !s.is_unique(), Err(_) => false, }; @@ -346,6 +348,25 @@ impl Solver { match program_clause { ProgramClause::Implies(implication) => { + let res = self.solve_via_implication( + canonical_goal, + Binders { + binders: vec![], + value: implication, + }, + minimums, + ); + if let Ok(solution) = res { + debug!("ok: solution={:?}", solution); + cur_solution = Some(match cur_solution { + None => solution, + Some(cur) => solution.combine(cur), + }); + } else { + debug!("error"); + } + } + ProgramClause::ForAll(implication) => { let res = self.solve_via_implication(canonical_goal, implication, minimums); if let Ok(solution) = res { debug!("ok: solution={:?}", solution); @@ -357,7 +378,6 @@ impl Solver { debug!("error"); } } - ProgramClause::ForAll(_) => todo!(), } } cur_solution.ok_or(NoSolution) @@ -387,8 +407,8 @@ impl Solver { fulfill.unify(&goal.environment, &goal.goal, &consequence)?; // if so, toss in all of its premises - for condition in conditions { - fulfill.push_goal(&goal.environment, condition)?; + for condition in conditions.as_slice() { + fulfill.push_goal(&goal.environment, condition.clone())?; } // and then try to solve From b10ae550f3e9a355cfb258af5fe9465da6f963e0 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 17:15:01 +0100 Subject: [PATCH 04/50] Fix more errors --- chalk-ir/src/lib.rs | 19 +++++ chalk-solve/src/recursive/fulfill.rs | 18 ++--- chalk-solve/src/recursive/mod.rs | 15 ++-- chalk-solve/src/recursive/stack.rs | 9 ++- chalk-solve/src/solve.rs | 112 +++++++++++++++++++++++++++ 5 files changed, 150 insertions(+), 23 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index f51e965596d..8317e554a4d 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -1466,6 +1466,25 @@ impl UCanonical { ); subst.is_identity_subst(interner) } + + pub fn trivial_substitution(&self, interner: &I) -> Substitution { + let binders = &self.canonical.binders; + Substitution::from( + binders + .iter() + .enumerate() + .map(|(index, pk)| match pk { + ParameterKind::Ty(_) => { + ParameterKind::Ty(TyData::BoundVar(index).intern(interner)).intern() + } + ParameterKind::Lifetime(_) => { + ParameterKind::Lifetime(LifetimeData::BoundVar(index).intern(interner)) + .intern() + } + }) + .collect::>(), + ) + } } #[derive(Clone, PartialEq, Eq, Hash, HasInterner)] diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index 81ada121d95..d67afe185dc 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -12,7 +12,6 @@ use infer::{ use interner::HasInterner; use std::collections::HashSet; use std::fmt::Debug; -use std::sync::Arc; use zip::Zip; enum Outcome { @@ -68,8 +67,8 @@ enum NegativeSolution { /// of type inference in general. But when solving trait constraints, *fresh* /// `Fulfill` instances will be created to solve canonicalized, free-standing /// goals, and transport what was learned back to the outer context. -pub(crate) struct Fulfill<'s, I: Interner> { - solver: &'s mut Solver<'s, I>, +pub(crate) struct Fulfill<'s, 'db, I: Interner> { + solver: &'s mut Solver<'db, I>, infer: InferenceTable, /// The remaining goals to prove or refute @@ -85,8 +84,8 @@ pub(crate) struct Fulfill<'s, I: Interner> { cannot_prove: bool, } -impl<'s, I: Interner> Fulfill<'s, I> { - pub(crate) fn new(solver: &'s mut Solver<'s, I>) -> Self { +impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { + pub(crate) fn new(solver: &'s mut Solver<'db, I>) -> Self { Fulfill { solver, infer: InferenceTable::new(), @@ -131,12 +130,7 @@ impl<'s, I: Interner> Fulfill<'s, I> { /// /// Wraps `InferenceTable::unify`; any resulting normalizations are added /// into our list of pending obligations with the given environment. - pub(crate) fn unify( - &mut self, - environment: &Arc>, - a: &T, - b: &T, - ) -> Fallible<()> + pub(crate) fn unify(&mut self, environment: &Environment, a: &T, b: &T) -> Fallible<()> where T: ?Sized + Zip + Debug, { @@ -155,7 +149,7 @@ impl<'s, I: Interner> Fulfill<'s, I> { /// ultimately create any number of obligations. pub(crate) fn push_goal( &mut self, - environment: &Arc>, + environment: &Environment, goal: Goal, ) -> Fallible<()> { debug!("push_goal({:?}, {:?})", goal, environment); diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 7535cac891a..bbc9c19790d 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -9,6 +9,7 @@ use self::search_graph::{DepthFirstNumber, SearchGraph}; use self::stack::{Stack, StackDepth}; use chalk_engine::fallible::{Fallible, NoSolution}; use chalk_ir::could_match::CouldMatch; +use clauses::program_clauses_for_goal; type UCanonicalGoal = UCanonical>>; @@ -119,7 +120,7 @@ impl<'me, I: Interner> Solver<'me, I> { // XXX how does caching with coinduction work? if self.stack.coinductive_cycle_from(depth) { let value = ConstrainedSubst { - subst: goal.trivial_substitution(), + subst: goal.trivial_substitution(self.program.interner()), constraints: vec![], }; debug!("applying coinductive semantics"); @@ -144,7 +145,7 @@ impl<'me, I: Interner> Solver<'me, I> { } else { // Otherwise, push the goal onto the stack and create a table. // The initial result for this table is error. - let depth = self.stack.push(&goal); + let depth = self.stack.push(self.program, &goal); let dfn = self.search_graph.insert(&goal, depth); let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn); self.search_graph[dfn].links = subgoal_minimums; @@ -245,13 +246,9 @@ impl<'me, I: Interner> Solver<'me, I> { let prog_solution = { debug_heading!("prog_clauses"); - let prog_clauses: Vec<_> = self - .program - .program_clauses - .iter() - .filter(|&clause| clause.could_match(goal)) - .cloned() - .collect(); + // TODO I think this includes clauses from env + let prog_clauses = + program_clauses_for_goal(self.program, environment, &goal); self.solve_from_clauses(&canonical_goal, prog_clauses, minimums) }; debug!("prog_solution={:?}", prog_solution); diff --git a/chalk-solve/src/recursive/stack.rs b/chalk-solve/src/recursive/stack.rs index 7d21fea4f72..0fca95f9050 100644 --- a/chalk-solve/src/recursive/stack.rs +++ b/chalk-solve/src/recursive/stack.rs @@ -1,4 +1,5 @@ use super::UCanonicalGoal; +use crate::{coinductive_goal::IsCoinductive, RustIrDatabase}; use chalk_ir::interner::Interner; use std::mem; use std::ops::Index; @@ -41,7 +42,11 @@ impl Stack { self.entries.is_empty() } - pub(crate) fn push(&mut self, goal: &UCanonicalGoal) -> StackDepth { + pub(crate) fn push( + &mut self, + program: &dyn RustIrDatabase, + goal: &UCanonicalGoal, + ) -> StackDepth { let depth = StackDepth { depth: self.entries.len(), }; @@ -53,7 +58,7 @@ impl Stack { panic!("overflow depth reached") } - let coinductive_goal = goal.is_coinductive(&self.program); + let coinductive_goal = goal.is_coinductive(program); self.entries.push(StackEntry { coinductive_goal, cycle: false, diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 75586678eec..58b61cc3a25 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -48,6 +48,118 @@ impl Solution { _ => false, } } + + /// There are multiple candidate solutions, which may or may not agree on + /// the values for existential variables; attempt to combine them. This + /// operation does not depend on the order of its arguments. + // + // This actually isn't as precise as it could be, in two ways: + // + // a. It might be that while there are multiple distinct candidates, they + // all agree about *some things*. To be maximally precise, we would + // compute the intersection of what they agree on. It's not clear though + // that this is actually what we want Rust's inference to do, and it's + // certainly not what it does today. + // + // b. There might also be an ambiguous candidate and a successful candidate, + // both with the same refined-goal. In that case, we could probably claim + // success, since if the conditions of the ambiguous candidate were met, + // we know the success would apply. Example: `?0: Clone` yields ambiguous + // candidate `Option: Clone` and successful candidate `Option: + // Clone`. + // + // But you get the idea. + pub(crate) fn combine(self, other: Solution) -> Solution { + use self::Guidance::*; + + if self == other { + return self; + } + + // Otherwise, always downgrade to Ambig: + + let guidance = match (self.into_guidance(), other.into_guidance()) { + (Definite(ref subst1), Definite(ref subst2)) if subst1 == subst2 => { + Definite(subst1.clone()) + } + (Suggested(ref subst1), Suggested(ref subst2)) if subst1 == subst2 => { + Suggested(subst1.clone()) + } + _ => Unknown, + }; + Solution::Ambig(guidance) + } + + /// There are multiple candidate solutions, which may or may not agree on + /// the values for existential variables; attempt to combine them, while + /// favoring `self` for the purposes of giving suggestions to type + /// inference. This is used in particular to favor the `where` clause + /// environment over `impl`s in guiding inference in ambiguous situations. + /// + /// It should always be the case that `x.favor_over(y)` is at least as + /// informative as `x.combine(y)`, in terms of guidance to type inference. + pub(crate) fn favor_over(self, other: Solution) -> Solution { + use self::Guidance::*; + + if self == other { + return self; + } + + // Otherwise, always downgrade to Ambig: + + let guidance = match (self.into_guidance(), other.into_guidance()) { + (Definite(subst), _) | (Suggested(subst), _) => Suggested(subst), + _ => Unknown, + }; + Solution::Ambig(guidance) + } + + /// View this solution purely in terms of type inference guidance + pub(crate) fn into_guidance(self) -> Guidance { + match self { + Solution::Unique(constrained) => Guidance::Definite(Canonical { + value: constrained.value.subst, + binders: constrained.binders, + }), + Solution::Ambig(guidance) => guidance, + } + } + + /// Extract a constrained substitution from this solution, even if ambiguous. + pub(crate) fn constrained_subst(&self) -> Option>> { + match *self { + Solution::Unique(ref constrained) => Some(constrained.clone()), + Solution::Ambig(Guidance::Definite(ref canonical)) + | Solution::Ambig(Guidance::Suggested(ref canonical)) => { + let value = ConstrainedSubst { + subst: canonical.value.clone(), + constraints: vec![], + }; + Some(Canonical { + value, + binders: canonical.binders.clone(), + }) + } + Solution::Ambig(_) => None, + } + } + + /// Determine whether this solution contains type information that *must* + /// hold. + pub(crate) fn has_definite(&self) -> bool { + match *self { + Solution::Unique(_) => true, + Solution::Ambig(Guidance::Definite(_)) => true, + _ => false, + } + } + + pub(crate) fn is_ambig(&self) -> bool { + match *self { + Solution::Ambig(_) => true, + _ => false, + } + } } impl fmt::Display for Solution { From d9e1a552001d75042797b6286775a3edfd8c401d Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 17:24:59 +0100 Subject: [PATCH 05/50] Fix another error --- chalk-solve/src/recursive/fulfill.rs | 35 +++++++++++----------------- chalk-solve/src/recursive/mod.rs | 8 +++---- 2 files changed, 16 insertions(+), 27 deletions(-) diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index d67afe185dc..f8cbe56c3e5 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -85,32 +85,23 @@ pub(crate) struct Fulfill<'s, 'db, I: Interner> { } impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { - pub(crate) fn new(solver: &'s mut Solver<'db, I>) -> Self { - Fulfill { + pub(crate) fn new + HasInterner + Clone>( + solver: &'s mut Solver<'db, I>, + ucanonical_goal: &UCanonical>, + ) -> (Self, Substitution, InEnvironment) { + let (infer, subst, canonical_goal) = InferenceTable::from_canonical( + solver.program.interner(), + ucanonical_goal.universes, + &ucanonical_goal.canonical, + ); + let fulfill = Fulfill { solver, - infer: InferenceTable::new(), + infer, obligations: vec![], constraints: HashSet::new(), cannot_prove: false, - } - } - - /// Given the canonical, initial goal, returns a substitution - /// that, when applied to this goal, will convert all of its bound - /// variables into fresh inference variables. The substitution can - /// then later be used as the answer to be returned to the user. - /// - /// See also `InferenceTable::fresh_subst`. - pub(crate) fn initial_subst + HasInterner>( - &mut self, - ucanonical_goal: &UCanonical>, - ) -> (Substitution, InEnvironment) { - let canonical_goal = self.infer.instantiate_universes(ucanonical_goal); - let subst = self - .infer - .fresh_subst(self.solver.program.interner(), &canonical_goal.binders); - let value = canonical_goal.substitute(&subst); - (subst, value) + }; + (fulfill, subst, canonical_goal) } /// Wraps `InferenceTable::instantiate_in` diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index bbc9c19790d..23b0c09c7e8 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -321,9 +321,8 @@ impl<'me, I: Interner> Solver<'me, I> { minimums: &mut Minimums, ) -> Fallible> { debug_heading!("solve_via_simplification({:?})", canonical_goal); - let mut fulfill = Fulfill::new(self); - let (subst, InEnvironment { environment, goal }) = fulfill.initial_subst(canonical_goal); - fulfill.push_goal(&environment, goal)?; + let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal); + fulfill.push_goal(&goal.environment, goal.goal)?; fulfill.solve(subst, minimums) } @@ -394,8 +393,7 @@ impl<'me, I: Interner> Solver<'me, I> { canonical_goal, clause ); - let mut fulfill = Fulfill::new(self); - let (subst, goal) = fulfill.initial_subst(canonical_goal); + let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal); let ProgramClauseImplication { consequence, conditions, From 22bfbc01655abdeb2eb66f115013372861148a89 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 17:28:29 +0100 Subject: [PATCH 06/50] Fix another error --- chalk-solve/src/infer/invert.rs | 17 +++++++++++++++++ chalk-solve/src/recursive/fulfill.rs | 2 +- 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/chalk-solve/src/infer/invert.rs b/chalk-solve/src/infer/invert.rs index 35ebe0a185d..227aef71aec 100644 --- a/chalk-solve/src/infer/invert.rs +++ b/chalk-solve/src/infer/invert.rs @@ -95,6 +95,23 @@ impl InferenceTable { .unwrap(); Some(inverted) } + + /// As `negated_instantiated`, but canonicalizes before + /// returning. Just a convenience function. + pub(crate) fn invert_then_canonicalize( + &mut self, + interner: &I, + value: &T, + ) -> Option> + where + T: Fold + HasInterner, + { + let snapshot = self.snapshot(); + let result = self.invert(interner, value); + let result = result.map(|r| self.canonicalize(interner, &r).quantified); + self.rollback_to(snapshot); + result + } } struct Inverter<'q, I: Interner> { diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index f8cbe56c3e5..e36ec0fa090 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -206,7 +206,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { } fn refute(&mut self, goal: &InEnvironment>) -> Fallible { - let canonicalized = match self.infer.invert_then_canonicalize(goal) { + let canonicalized = match self.infer.invert_then_canonicalize(self.interner(), goal) { Some(v) => v, None => { // Treat non-ground negatives as ambiguous. Note that, as inference From 82094769ab5419f787194dbbb0501b556c03ef25 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 17:33:47 +0100 Subject: [PATCH 07/50] Fix the next error, method resolution succeeds --- chalk-solve/src/infer.rs | 26 ++++++++++++++++++++++++++ chalk-solve/src/recursive/fulfill.rs | 2 +- 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/chalk-solve/src/infer.rs b/chalk-solve/src/infer.rs index f9efbca5852..5b9af119b68 100644 --- a/chalk-solve/src/infer.rs +++ b/chalk-solve/src/infer.rs @@ -199,6 +199,32 @@ impl InferenceTable { InferenceValue::Bound(_) => panic!("var_universe invoked on bound variable"), } } + + /// Check whether the given substitution is the identity substitution in this + /// inference context. + pub(crate) fn is_trivial_substitution(&mut self, subst: &Substitution) -> bool { + for value in subst.as_parameters() { + match value.data() { + ParameterKind::Ty(ty) => { + if let Some(var) = ty.inference_var() { + if self.var_is_bound(var) { + return false; + } + } + } + + ParameterKind::Lifetime(lifetime) => { + if let Some(var) = lifetime.inference_var() { + if self.var_is_bound(var) { + return false; + } + } + } + } + } + + true + } } pub(crate) trait ParameterEnaVariableExt { diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index e36ec0fa090..24bd8828ec7 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -372,7 +372,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { // need to determine how to package up what we learned about type // inference as an ambiguous solution. - if subst.is_trivial_within(&mut self.infer) { + if self.infer.is_trivial_substitution(&subst) { // In this case, we didn't learn *anything* definitively. So now, we // go one last time through the positive obligations, this time // applying even *tentative* inference suggestions, so that we can From 311eb337fc58b00b03c719f3645ffa64ed920ae5 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 17:38:04 +0100 Subject: [PATCH 08/50] Fix remaining errors --- chalk-solve/src/recursive/fulfill.rs | 47 ++++++++++++++++++---------- chalk-solve/src/recursive/mod.rs | 6 ++-- 2 files changed, 34 insertions(+), 19 deletions(-) diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index 24bd8828ec7..f735de7d92b 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -126,7 +126,8 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { T: ?Sized + Zip + Debug, { let UnificationResult { goals, constraints } = - self.infer.unify(self.interner(), environment, a, b)?; + self.infer + .unify(self.solver.program.interner(), environment, a, b)?; debug!("unify({:?}, {:?}) succeeded", a, b); debug!("unify: goals={:?}", goals); debug!("unify: constraints={:?}", constraints); @@ -148,18 +149,18 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { GoalData::Quantified(QuantifierKind::ForAll, subgoal) => { let subgoal = self .infer - .instantiate_binders_universally(self.interner(), subgoal); + .instantiate_binders_universally(self.solver.program.interner(), subgoal); self.push_goal(environment, subgoal)?; } GoalData::Quantified(QuantifierKind::Exists, subgoal) => { let subgoal = self .infer - .instantiate_binders_existentially(self.interner(), subgoal); + .instantiate_binders_existentially(self.solver.program.interner(), subgoal); self.push_goal(environment, subgoal)?; } GoalData::Implies(wc, subgoal) => { let new_environment = &environment.add_clauses(wc.iter().cloned()); - self.push_goal(new_environment, *subgoal)?; + self.push_goal(new_environment, subgoal.clone())?; } GoalData::All(goals) => { for subgoal in goals.as_slice() { @@ -167,7 +168,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { } } GoalData::Not(subgoal) => { - let in_env = InEnvironment::new(environment, *subgoal); + let in_env = InEnvironment::new(environment, subgoal.clone()); self.obligations.push(Obligation::Refute(in_env)); } GoalData::DomainGoal(_) => { @@ -189,15 +190,16 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { wc: &InEnvironment>, minimums: &mut Minimums, ) -> Fallible> { + let interner = self.solver.program.interner(); let Canonicalized { quantified, free_vars, - max_universe: _, - } = self.infer.canonicalize(self.interner(), wc); + .. + } = self.infer.canonicalize(interner, wc); let UCanonicalized { quantified, universes, - } = self.infer.u_canonicalize(self.interner(), &quantified); + } = self.infer.u_canonicalize(interner, &quantified); Ok(PositiveSolution { free_vars, universes, @@ -206,7 +208,10 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { } fn refute(&mut self, goal: &InEnvironment>) -> Fallible { - let canonicalized = match self.infer.invert_then_canonicalize(self.interner(), goal) { + let canonicalized = match self + .infer + .invert_then_canonicalize(self.solver.program.interner(), goal) + { Some(v) => v, None => { // Treat non-ground negatives as ambiguous. Note that, as inference @@ -219,7 +224,9 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let UCanonicalized { quantified, universes: _, - } = self.infer.u_canonicalize(self.interner(), &canonicalized); + } = self + .infer + .u_canonicalize(self.solver.program.interner(), &canonicalized); let mut minimums = Minimums::new(); // FIXME -- minimums here seems wrong if let Ok(solution) = self.solver.solve_goal(quantified, &mut minimums) { if solution.is_unique() { @@ -247,8 +254,9 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { subst: Canonical>, ) { let subst = universes.map_from_canonical(self.interner(), &subst); - let ConstrainedSubst { subst, constraints } = - self.infer.instantiate_canonical(self.interner(), &subst); + let ConstrainedSubst { subst, constraints } = self + .infer + .instantiate_canonical(self.solver.program.interner(), &subst); debug!( "fulfill::apply_solution: adding constraints {:?}", @@ -361,9 +369,10 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { // and the current inference state is the unique way to solve them. let constraints = self.constraints.into_iter().collect(); - let constrained = self - .infer - .canonicalize(self.interner(), &ConstrainedSubst { subst, constraints }); + let constrained = self.infer.canonicalize( + self.solver.program.interner(), + &ConstrainedSubst { subst, constraints }, + ); return Ok(Solution::Unique(constrained.quantified)); } @@ -389,7 +398,9 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { } = self.prove(&goal, minimums).unwrap(); if let Some(constrained_subst) = solution.constrained_subst() { self.apply_solution(free_vars, universes, constrained_subst); - let subst = self.infer.canonicalize(self.interner(), &subst); + let subst = self + .infer + .canonicalize(self.solver.program.interner(), &subst); return Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))); } } @@ -417,7 +428,9 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { // for sure what `T` must be (it could be either `Foo` or // `Foo`, but we *can* say for sure that it must be of the // form `Foo`. - let subst = self.infer.canonicalize(self.interner(), &subst); + let subst = self + .infer + .canonicalize(self.solver.program.interner(), &subst); Ok(Solution::Ambig(Guidance::Definite(subst.quantified))) } } diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 23b0c09c7e8..6d7439f8c0b 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -1,3 +1,5 @@ +#![allow(unused)] + use super::*; mod fulfill; @@ -11,7 +13,7 @@ use chalk_engine::fallible::{Fallible, NoSolution}; use chalk_ir::could_match::CouldMatch; use clauses::program_clauses_for_goal; -type UCanonicalGoal = UCanonical>>; +type UCanonicalGoal = UCanonical>>; /// A Solver is the basic context in which you can propose goals for a given /// program. **All questions posed to the solver are in canonical, closed form, @@ -296,7 +298,7 @@ impl<'me, I: Interner> Solver<'me, I> { } let current_answer_is_ambig = match ¤t_answer { - Ok(s) => !s.is_unique(), + Ok(s) => s.is_ambig(), Err(_) => false, }; From 298c3b97f81daa7a63158422e687985f733854ae Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 17:53:27 +0100 Subject: [PATCH 09/50] Add recursive solver to SolverChoice --- chalk-solve/src/recursive/mod.rs | 77 ++++++++++++++++++-------------- chalk-solve/src/solve.rs | 65 ++++++++++++++++++++++----- 2 files changed, 96 insertions(+), 46 deletions(-) diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 6d7439f8c0b..bda98c5673b 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -1,5 +1,3 @@ -#![allow(unused)] - use super::*; mod fulfill; @@ -15,6 +13,13 @@ use clauses::program_clauses_for_goal; type UCanonicalGoal = UCanonical>>; +pub(crate) struct RecursiveContext { + stack: Stack, + search_graph: SearchGraph, + + caching_enabled: bool, +} + /// A Solver is the basic context in which you can propose goals for a given /// program. **All questions posed to the solver are in canonical, closed form, /// so that each question is answered with effectively a "clean slate"**. This @@ -22,10 +27,7 @@ type UCanonicalGoal = UCanonical>>; /// context. pub(crate) struct Solver<'me, I: Interner> { program: &'me dyn RustIrDatabase, - stack: Stack, - search_graph: SearchGraph, - - caching_enabled: bool, + context: &'me mut RecursiveContext, } /// The `minimums` struct is used while solving to track whether we encountered @@ -55,20 +57,27 @@ impl MergeWith for Fallible { } } -impl<'me, I: Interner> Solver<'me, I> { - pub(crate) fn new( - program: &'me dyn RustIrDatabase, - overflow_depth: usize, - caching_enabled: bool, - ) -> Self { - Solver { - program, +impl RecursiveContext { + pub(crate) fn new(overflow_depth: usize, caching_enabled: bool) -> Self { + RecursiveContext { stack: Stack::new(overflow_depth), search_graph: SearchGraph::new(), caching_enabled, } } + pub(crate) fn solver<'me>( + &'me mut self, + program: &'me dyn RustIrDatabase, + ) -> Solver<'me, I> { + Solver { + program, + context: self, + } + } +} + +impl<'me, I: Interner> Solver<'me, I> { /// Solves a canonical goal. The substitution returned in the /// solution will be for the fully decomposed goal. For example, given the /// program @@ -89,7 +98,7 @@ impl<'me, I: Interner> Solver<'me, I> { canonical_goal: &UCanonicalGoal, ) -> Fallible> { debug!("solve_root_goal(canonical_goal={:?})", canonical_goal); - assert!(self.stack.is_empty()); + assert!(self.context.stack.is_empty()); let minimums = &mut Minimums::new(); self.solve_goal(canonical_goal.clone(), minimums) } @@ -112,15 +121,15 @@ impl<'me, I: Interner> Solver<'me, I> { // } // Next, check if the goal is in the search tree already. - if let Some(dfn) = self.search_graph.lookup(&goal) { + if let Some(dfn) = self.context.search_graph.lookup(&goal) { // Check if this table is still on the stack. - if let Some(depth) = self.search_graph[dfn].stack_depth { + 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? - if self.stack.coinductive_cycle_from(depth) { + if self.context.stack.coinductive_cycle_from(depth) { let value = ConstrainedSubst { subst: goal.trivial_substitution(self.program.interner()), constraints: vec![], @@ -132,13 +141,13 @@ impl<'me, I: Interner> Solver<'me, I> { })); } - self.stack[depth].flag_cycle(); + self.context.stack[depth].flag_cycle(); } - minimums.update_from(self.search_graph[dfn].links); + minimums.update_from(self.context.search_graph[dfn].links); // Return the solution from the table. - let previous_solution = self.search_graph[dfn].solution.clone(); + let previous_solution = self.context.search_graph[dfn].solution.clone(); debug!( "solve_goal: cycle detected, previous solution {:?}", previous_solution @@ -147,23 +156,23 @@ impl<'me, I: Interner> Solver<'me, I> { } else { // Otherwise, push the goal onto the stack and create a table. // The initial result for this table is error. - let depth = self.stack.push(self.program, &goal); - let dfn = self.search_graph.insert(&goal, depth); + let depth = self.context.stack.push(self.program, &goal); + let dfn = self.context.search_graph.insert(&goal, depth); let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn); - self.search_graph[dfn].links = subgoal_minimums; - self.search_graph[dfn].stack_depth = None; - self.stack.pop(depth); + self.context.search_graph[dfn].links = subgoal_minimums; + self.context.search_graph[dfn].stack_depth = None; + self.context.stack.pop(depth); minimums.update_from(subgoal_minimums); // Read final result from table. - let result = self.search_graph[dfn].solution.clone(); + let result = self.context.search_graph[dfn].solution.clone(); // If processing this subgoal did not involve anything // outside of its subtree, then we can promote it to the // cache now. This is a sort of hack to alleviate the // worst of the repeated work that we do during tabling. if subgoal_minimums.positive >= dfn { - if self.caching_enabled { + if self.context.caching_enabled { // TODO // self.search_graph.move_to_cache(dfn, &mut self.cache); debug!("solve_reduced_goal: SCC head encountered, moving to cache"); @@ -171,7 +180,7 @@ impl<'me, I: Interner> Solver<'me, I> { debug!( "solve_reduced_goal: SCC head encountered, rolling back as caching disabled" ); - self.search_graph.rollback_to(dfn); + self.context.search_graph.rollback_to(dfn); } } @@ -283,16 +292,16 @@ impl<'me, I: Interner> Solver<'me, I> { current_answer, minimums ); - if !self.stack[depth].read_and_reset_cycle_flag() { + if !self.context.stack[depth].read_and_reset_cycle_flag() { // None of our subgoals depended on us directly. // We can return. - self.search_graph[dfn].solution = current_answer; + self.context.search_graph[dfn].solution = current_answer; return *minimums; } // Some of our subgoals depended on us. We need to re-run // with the current answer. - if self.search_graph[dfn].solution == current_answer { + if self.context.search_graph[dfn].solution == current_answer { // Reached a fixed point. return *minimums; } @@ -302,7 +311,7 @@ impl<'me, I: Interner> Solver<'me, I> { Err(_) => false, }; - self.search_graph[dfn].solution = current_answer; + self.context.search_graph[dfn].solution = current_answer; // Subtle: if our current answer is ambiguous, we can just // stop, and in fact we *must* -- otherwise, wesometimes @@ -313,7 +322,7 @@ impl<'me, I: Interner> Solver<'me, I> { } // Otherwise: rollback the search tree and try again. - self.search_graph.rollback_to(dfn + 1); + self.context.search_graph.rollback_to(dfn + 1); } } diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 58b61cc3a25..5027d8980c0 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -1,5 +1,5 @@ use crate::solve::slg::SlgContext; -use crate::RustIrDatabase; +use crate::{recursive::RecursiveContext, RustIrDatabase}; use chalk_engine::forest::{Forest, SubstitutionResult}; use chalk_ir::interner::Interner; use chalk_ir::*; @@ -184,6 +184,11 @@ pub enum SolverChoice { max_size: usize, expected_answers: Option, }, + /// Run the recursive solver. + Recursive { + overflow_depth: usize, + caching_enabled: bool, + }, } impl SolverChoice { @@ -195,15 +200,30 @@ impl SolverChoice { } } + /// Returns the default recursive solver setup. + pub fn recursive() -> Self { + SolverChoice::Recursive { + overflow_depth: 100, + caching_enabled: true, + } + } + /// Creates a solver state. pub fn into_solver(self) -> Solver { match self { SolverChoice::SLG { max_size, expected_answers, - } => Solver { - forest: Forest::new(SlgContext::new(max_size, expected_answers)), - }, + } => Solver(SolverImpl::Slg { + forest: Box::new(Forest::new(SlgContext::new(max_size, expected_answers))), + }), + SolverChoice::Recursive { + overflow_depth, + caching_enabled, + } => Solver(SolverImpl::Recursive(Box::new(RecursiveContext::new( + overflow_depth, + caching_enabled, + )))), } } } @@ -218,8 +238,11 @@ impl Default for SolverChoice { /// out what sets of types implement which traits. Also, between /// queries, this struct stores the cached state from previous solver /// attempts, which can then be re-used later. -pub struct Solver { - forest: Forest>, +pub struct Solver(SolverImpl); + +enum SolverImpl { + Slg { forest: Box>> }, + Recursive(Box>), } impl Solver { @@ -246,8 +269,13 @@ impl Solver { program: &dyn RustIrDatabase, goal: &UCanonical>>, ) -> Option> { - let ops = self.forest.context().ops(program); - self.forest.solve(&ops, goal, || true) + match &mut self.0 { + SolverImpl::Slg { forest } => { + let ops = forest.context().ops(program); + forest.solve(&ops, goal, || true) + } + SolverImpl::Recursive(ctx) => ctx.solver(program).solve_root_goal(goal).ok(), + } } /// Attempts to solve the given goal, which must be in canonical @@ -278,8 +306,16 @@ impl Solver { goal: &UCanonical>>, should_continue: impl std::ops::Fn() -> bool, ) -> Option> { - let ops = self.forest.context().ops(program); - self.forest.solve(&ops, goal, should_continue) + match &mut self.0 { + SolverImpl::Slg { forest } => { + let ops = forest.context().ops(program); + forest.solve(&ops, goal, should_continue) + } + SolverImpl::Recursive(ctx) => { + // TODO support should_continue in recursive solver + ctx.solver(program).solve_root_goal(goal).ok() + } + } } /// Attempts to solve the given goal, which must be in canonical @@ -310,8 +346,13 @@ impl Solver { goal: &UCanonical>>, f: impl FnMut(SubstitutionResult>>, bool) -> bool, ) -> bool { - let ops = self.forest.context().ops(program); - self.forest.solve_multiple(&ops, goal, f) + match &mut self.0 { + SolverImpl::Slg { forest } => { + let ops = forest.context().ops(program); + forest.solve_multiple(&ops, goal, f) + } + SolverImpl::Recursive(_ctx) => unimplemented!(), + } } } From d3267cf2552ff98d7ee4d6baae6ecf6649f91b77 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 17:59:38 +0100 Subject: [PATCH 10/50] Temporary: Use recursive solver by default in tests --- chalk-solve/src/solve.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 5027d8980c0..dd980ad164a 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -230,7 +230,8 @@ impl SolverChoice { impl Default for SolverChoice { fn default() -> Self { - SolverChoice::slg(10, None) + SolverChoice::recursive() + // SolverChoice::slg(10, None) } } From 52dc02a72e61f61eff26c5a2c24fe4e44d449d95 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 8 Mar 2020 18:08:25 +0100 Subject: [PATCH 11/50] Delete unused file --- chalk-solve/src/recursive/tables.rs | 59 ----------------------------- 1 file changed, 59 deletions(-) delete mode 100644 chalk-solve/src/recursive/tables.rs diff --git a/chalk-solve/src/recursive/tables.rs b/chalk-solve/src/recursive/tables.rs deleted file mode 100644 index 42e27755603..00000000000 --- a/chalk-solve/src/recursive/tables.rs +++ /dev/null @@ -1,59 +0,0 @@ -use fallible::*; -use std::ops::Index; -use std::ops::IndexMut; - -use super::stack::StackDepth; - -// TODO this file doesn't seem used - -#[derive(Default)] -pub(crate) struct Tables { - indices: HashMap, - tables: Vec
, -} - -pub(crate) struct TableIndex { - index: usize, -} - -pub(crate) struct Table { - pub(crate) solution: Fallible, - pub(crate) stack_depth: Option, -} - -impl Tables { - pub(crate) fn lookup(&self, goal: &CanonicalLeafGoal) -> Option { - self.indices.get(goal) - } - - pub(crate) fn insert( - &mut self, - goal: &CanonicalLeafGoal, - solution: Fallible, - stack_depth: Option, - ) -> TableIndex { - let table = Table { - solution, - stack_depth, - }; - let index = self.tables.len(); - self.tables.push(table); - let previous_index = self.indices.insert(goal.clone(), index); - assert!(previous_index.is_none()); - TableIndex { index } - } -} - -impl Index for Tables { - type Output = Table; - - fn index(&self, table_index: TableIndex) -> &Table { - &self.tables[table_index.index] - } -} - -impl IndexMut for Tables { - fn index(&self, table_index: TableIndex) -> &mut Table { - &self.tables[table_index.index] - } -} From faae7fd92668a2810f7d5f5b31f60fc2d7d0d1ff Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Wed, 11 Mar 2020 21:22:55 +0100 Subject: [PATCH 12/50] Fix dyn_Foo_Bar failure --- chalk-solve/src/clauses.rs | 100 +++++++++++++++++++++++++++---- chalk-solve/src/recursive/mod.rs | 7 +-- 2 files changed, 90 insertions(+), 17 deletions(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 21c10595aaf..01ad3ad4f3d 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -222,19 +222,24 @@ fn program_clauses_that_could_match( // and `bounded_ty` is the `exists { .. }` // clauses shown above. - for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) { - // Replace the `T` from `exists { .. }` with `self_ty`, - // yielding clases like - // - // ``` - // forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) } - // ``` - let qwc = exists_qwc.substitute(interner, &[self_ty.clone().cast(interner)]); - - builder.push_binders(&qwc, |builder, wc| { - builder.push_fact(wc); - }); - } + let generalized_dyn_ty = generalize::Generalize::apply(db.interner(), dyn_ty); + + builder.push_binders(&generalized_dyn_ty, |builder, dyn_ty| { + for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) { + // Replace the `T` from `exists { .. }` with `self_ty`, + // yielding clases like + // + // ``` + // forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) } + // ``` + let qwc = + exists_qwc.substitute(interner, &[self_ty.clone().cast(interner)]); + + builder.push_binders(&qwc, |builder, wc| { + builder.push_fact(wc); + }); + } + }); } if let Some(well_known) = trait_datum.well_known { @@ -416,3 +421,72 @@ fn program_clauses_for_env<'db, I: Interner>( clauses.extend(closure.drain()) } + +mod generalize { + use chalk_engine::fallible::Fallible; + use chalk_ir::{ + fold::{Fold, Folder}, + interner::Interner, + Binders, Lifetime, LifetimeData, ParameterKind, Ty, TyData, + }; + use std::collections::HashMap; + + pub struct Generalize<'i, I: Interner> { + binders: Vec>, + mapping: HashMap, + interner: &'i I, + } + + impl Generalize<'_, I> { + pub fn apply>(interner: &I, value: &T) -> Binders { + let mut generalize = Generalize { + binders: Vec::new(), + mapping: HashMap::new(), + interner, + }; + let value = value.fold_with(&mut generalize, 0).unwrap(); + Binders { + binders: generalize.binders, + value, + } + } + } + + impl Folder for Generalize<'_, I> { + fn as_dyn(&mut self) -> &mut dyn Folder { + self + } + + fn fold_free_var_ty(&mut self, depth: usize, binders: usize) -> Fallible> { + let binder_vec = &mut self.binders; + let new_index = self.mapping.entry(depth).or_insert_with(|| { + let i = binder_vec.len(); + binder_vec.push(ParameterKind::Ty(())); + i + }); + Ok(TyData::BoundVar(*new_index + binders).intern(self.interner())) + } + + fn fold_free_var_lifetime( + &mut self, + depth: usize, + binders: usize, + ) -> Fallible> { + let binder_vec = &mut self.binders; + let new_index = self.mapping.entry(depth).or_insert_with(|| { + let i = binder_vec.len(); + binder_vec.push(ParameterKind::Ty(())); + i + }); + Ok(LifetimeData::BoundVar(*new_index + binders).intern(self.interner())) + } + + fn interner(&self) -> &I { + self.interner + } + + fn target_interner(&self) -> &I { + self.interner() + } + } +} diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index bda98c5673b..e283b469505 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -313,10 +313,9 @@ impl<'me, I: Interner> Solver<'me, I> { self.context.search_graph[dfn].solution = current_answer; - // Subtle: if our current answer is ambiguous, we can just - // stop, and in fact we *must* -- otherwise, wesometimes - // fail to reach a fixed point. See - // `multiple_ambiguous_cycles` for more. + // Subtle: if our current answer is ambiguous, we can just stop, and + // in fact we *must* -- otherwise, we sometimes fail to reach a + // fixed point. See `multiple_ambiguous_cycles` for more. if current_answer_is_ambig { return *minimums; } From 30fe8c5b1fe5568d21545f3ab6c07eb9275c4a89 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 17 Mar 2020 13:42:23 +0100 Subject: [PATCH 13/50] Clause priorities (WIP) --- chalk-integration/src/lowering.rs | 5 ++- chalk-ir/src/cast.rs | 2 + chalk-ir/src/fold/boring_impls.rs | 1 + chalk-ir/src/lib.rs | 8 ++++ chalk-ir/src/zip.rs | 4 +- chalk-solve/src/clauses/builder.rs | 26 +++++++++++ chalk-solve/src/clauses/program_clauses.rs | 2 +- chalk-solve/src/recursive/mod.rs | 50 ++++++++++++++++++---- chalk-solve/src/solve.rs | 4 ++ chalk-solve/src/solve/slg/resolvent.rs | 5 ++- tests/test/mod.rs | 12 ++++++ tests/test/projection.rs | 6 +++ 12 files changed, 111 insertions(+), 14 deletions(-) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 7345e49cc42..1d79771e975 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -1,8 +1,8 @@ use chalk_ir::cast::{Cast, Caster}; use chalk_ir::interner::ChalkIr; use chalk_ir::{ - self, AssocTypeId, BoundVar, DebruijnIndex, ImplId, QuantifiedWhereClauses, StructId, - Substitution, TraitId, + self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, QuantifiedWhereClauses, + StructId, Substitution, TraitId, }; use chalk_parse::ast::*; use chalk_rust_ir as rust_ir; @@ -1193,6 +1193,7 @@ impl LowerClause for Clause { .map(|consequence| chalk_ir::ProgramClauseImplication { consequence, conditions: conditions.clone(), + priority: ClausePriority::High, }) .collect::>(); Ok(implications) diff --git a/chalk-ir/src/cast.rs b/chalk-ir/src/cast.rs index 3f637378ae1..052ead6b6e2 100644 --- a/chalk-ir/src/cast.rs +++ b/chalk-ir/src/cast.rs @@ -187,6 +187,7 @@ where ProgramClauseData::Implies(ProgramClauseImplication { consequence: self.cast(interner), conditions: Goals::new(interner), + priority: ClausePriority::High, }) .intern(interner) } @@ -201,6 +202,7 @@ where ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication { consequence: bound.cast(interner), conditions: Goals::new(interner), + priority: ClausePriority::High, })) .intern(interner) } diff --git a/chalk-ir/src/fold/boring_impls.rs b/chalk-ir/src/fold/boring_impls.rs index 9e5d114af0e..becd861befd 100644 --- a/chalk-ir/src/fold/boring_impls.rs +++ b/chalk-ir/src/fold/boring_impls.rs @@ -243,6 +243,7 @@ copy_fold!(DebruijnIndex); copy_fold!(chalk_engine::TableIndex); copy_fold!(chalk_engine::TimeStamp); copy_fold!(()); +copy_fold!(ClausePriority); #[macro_export] macro_rules! id_fold { diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 8317e554a4d..fb4b5eaae12 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -1304,6 +1304,13 @@ impl Iterator for BindersIntoIterator { pub struct ProgramClauseImplication { pub consequence: DomainGoal, pub conditions: Goals, + pub priority: ClausePriority, +} + +#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)] +pub enum ClausePriority { + High, + Low, } #[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner)] @@ -1318,6 +1325,7 @@ impl ProgramClauseImplication { ProgramClauseImplication { consequence: self.consequence.into_from_env_goal(interner), conditions: self.conditions.clone(), + priority: self.priority, } } else { self diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs index 5159ddc078c..956d0b0a0a0 100644 --- a/chalk-ir/src/zip.rs +++ b/chalk-ir/src/zip.rs @@ -200,6 +200,7 @@ eq_zip!(I => TypeName); eq_zip!(I => QuantifierKind); eq_zip!(I => PhantomData); eq_zip!(I => PlaceholderIndex); +eq_zip!(I => ClausePriority); /// Generates a Zip impl that zips each field of the struct in turn. macro_rules! struct_zip { @@ -242,7 +243,8 @@ struct_zip!(impl[I: Interner] Zip for AliasEq { alias, ty }); struct_zip!(impl[I: Interner] Zip for EqGoal { a, b }); struct_zip!(impl[I: Interner] Zip for ProgramClauseImplication { consequence, - conditions + conditions, + priority, }); impl Zip for Environment { diff --git a/chalk-solve/src/clauses/builder.rs b/chalk-solve/src/clauses/builder.rs index 0a8a1327517..4851af21ee4 100644 --- a/chalk-solve/src/clauses/builder.rs +++ b/chalk-solve/src/clauses/builder.rs @@ -35,6 +35,18 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> { self.push_clause(consequence, None::>); } + /// Pushes a "fact" `forall<..> { consequence }` into the set of + /// program clauses, meaning something that we can assume to be + /// true unconditionally. The `forall<..>` binders will be + /// whichever binders have been pushed (see `push_binders`). + pub fn push_fact_with_priority( + &mut self, + consequence: impl CastTo>, + priority: ClausePriority, + ) { + self.push_clause_with_priority(consequence, None::>, priority); + } + /// Pushes a clause `forall<..> { consequence :- conditions }` /// into the set of program clauses, meaning that `consequence` /// can be proven if `conditions` are all true. The `forall<..>` @@ -43,11 +55,25 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> { &mut self, consequence: impl CastTo>, conditions: impl IntoIterator>>, + ) { + self.push_clause_with_priority(consequence, conditions, ClausePriority::High) + } + + /// Pushes a clause `forall<..> { consequence :- conditions }` + /// into the set of program clauses, meaning that `consequence` + /// can be proven if `conditions` are all true. The `forall<..>` + /// binders will be whichever binders have been pushed (see `push_binders`). + pub fn push_clause_with_priority( + &mut self, + consequence: impl CastTo>, + conditions: impl IntoIterator>>, + priority: ClausePriority, ) { let interner = self.db.interner(); let clause = ProgramClauseImplication { consequence: consequence.cast(interner), conditions: Goals::from(interner, conditions), + priority, }; if self.binders.len() == 0 { diff --git a/chalk-solve/src/clauses/program_clauses.rs b/chalk-solve/src/clauses/program_clauses.rs index 3b606f31a54..b76c2da2d8c 100644 --- a/chalk-solve/src/clauses/program_clauses.rs +++ b/chalk-solve/src/clauses/program_clauses.rs @@ -612,7 +612,7 @@ impl ToProgramClauses for AssociatedTyDatum { // forall { // AliasEq(::Assoc = (Foo::Assoc)). // } - builder.push_fact(alias_eq); + builder.push_fact_with_priority(alias_eq, ClausePriority::Low); // Well-formedness of projection type. // diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index e283b469505..0d1b732c34e 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -245,6 +245,7 @@ impl<'me, I: Interner> Solver<'me, I> { let env_solution = { debug_heading!("env_clauses"); + // TODO use code from clauses module let env_clauses = environment .clauses .iter() @@ -257,7 +258,7 @@ impl<'me, I: Interner> Solver<'me, I> { let prog_solution = { debug_heading!("prog_clauses"); - // TODO I think this includes clauses from env + // TODO this also includes clauses from env let prog_clauses = program_clauses_for_goal(self.program, environment, &goal); self.solve_from_clauses(&canonical_goal, prog_clauses, minimums) @@ -349,11 +350,36 @@ impl<'me, I: Interner> Solver<'me, I> { C: IntoIterator>, { let mut cur_solution = None; + fn combine_with_priorities( + a: Solution, + prio_a: ClausePriority, + b: Solution, + prio_b: ClausePriority, + ) -> (Solution, ClausePriority) { + match (prio_a, prio_b) { + (ClausePriority::High, ClausePriority::Low) => { + debug!( + "preferring solution: {:?} over {:?} because of higher prio", + a, b + ); + (a, ClausePriority::High) + } + (ClausePriority::Low, ClausePriority::High) => { + debug!( + "preferring solution: {:?} over {:?} because of higher prio", + b, a + ); + (b, ClausePriority::High) + } + _ => (a.combine(b), prio_a), + } + } for program_clause in clauses { debug_heading!("clause={:?}", program_clause); match program_clause { ProgramClause::Implies(implication) => { + let priority = implication.priority; let res = self.solve_via_implication( canonical_goal, Binders { @@ -363,22 +389,27 @@ impl<'me, I: Interner> Solver<'me, I> { minimums, ); if let Ok(solution) = res { - debug!("ok: solution={:?}", solution); + debug!("ok: solution={:?} prio={:?}", solution, priority); cur_solution = Some(match cur_solution { - None => solution, - Some(cur) => solution.combine(cur), + None => (solution, priority), + Some((cur, cur_priority)) => { + combine_with_priorities(cur, cur_priority, solution, priority) + } }); } else { debug!("error"); } } ProgramClause::ForAll(implication) => { + let priority = implication.value.priority; let res = self.solve_via_implication(canonical_goal, implication, minimums); if let Ok(solution) = res { - debug!("ok: solution={:?}", solution); + debug!("ok: solution={:?} prio={:?}", solution, priority); cur_solution = Some(match cur_solution { - None => solution, - Some(cur) => solution.combine(cur), + None => (solution, priority), + Some((cur, cur_priority)) => { + combine_with_priorities(cur, cur_priority, solution, priority) + } }); } else { debug!("error"); @@ -386,7 +417,7 @@ impl<'me, I: Interner> Solver<'me, I> { } } } - cur_solution.ok_or(NoSolution) + cur_solution.map(|(s, _)| s).ok_or(NoSolution) } /// Modus ponens! That is: try to apply an implication by proving its premises. @@ -407,8 +438,11 @@ impl<'me, I: Interner> Solver<'me, I> { let ProgramClauseImplication { consequence, conditions, + priority: _, } = fulfill.instantiate_binders_existentially(&clause); + debug!("the subst is {:?}", subst); + fulfill.unify(&goal.environment, &goal.goal, &consequence)?; // if so, toss in all of its premises diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index dd980ad164a..970728b1bf1 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -76,6 +76,8 @@ impl Solution { return self; } + debug!("combine {} with {}", self, other); + // Otherwise, always downgrade to Ambig: let guidance = match (self.into_guidance(), other.into_guidance()) { @@ -105,6 +107,8 @@ impl Solution { return self; } + debug!("favor_over {} with {}", self, other); + // Otherwise, always downgrade to Ambig: let guidance = match (self.into_guidance(), other.into_guidance()) { diff --git a/chalk-solve/src/solve/slg/resolvent.rs b/chalk-solve/src/solve/slg/resolvent.rs index 65c002f0330..6c0478e406f 100644 --- a/chalk-solve/src/solve/slg/resolvent.rs +++ b/chalk-solve/src/solve/slg/resolvent.rs @@ -83,9 +83,10 @@ impl context::ResolventOps> for TruncatingInferenceTa let ProgramClauseImplication { consequence, conditions, + priority: _, } = match clause.data(interner) { - ProgramClauseData::Implies(implication) => implication.clone(), - ProgramClauseData::ForAll(implication) => self + ProgramClause::Implies(implication) => implication.clone(), + ProgramClause::ForAll(implication) => self .infer .instantiate_binders_existentially(interner, implication), }; diff --git a/tests/test/mod.rs b/tests/test/mod.rs index f1db8e262cb..52fcddd8487 100644 --- a/tests/test/mod.rs +++ b/tests/test/mod.rs @@ -200,6 +200,18 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>) { let program = db.checked_program().unwrap(); for (goal_text, solver_choice, expected) in goals { + match (&solver_choice, &expected) { + (SolverChoice::Recursive { .. }, TestGoal::All(_)) + | (SolverChoice::Recursive { .. }, TestGoal::First(_)) => { + println!( + "skipping goal {} for recursive solver because it requires solve_multiple", + goal_text + ); + continue; + } + _ => {} + }; + if db.solver_choice() != solver_choice { db.set_solver_choice(solver_choice); } diff --git a/tests/test/projection.rs b/tests/test/projection.rs index 38240ab8c52..fcf09a36388 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -76,6 +76,7 @@ fn normalize_basic() { "Unique" } + /* TODO: this doesn't seem to be correct, actually goal { forall { if (T: Iterator) { @@ -88,6 +89,7 @@ fn normalize_basic() { // True for `U = T`, of course, but also true for `U = Vec`. "Ambiguous" } + */ } } @@ -444,6 +446,7 @@ fn normalize_under_binder() { } } + /* TODO: this doesn't seem to be correct, actually goal { exists { forall<'a> { @@ -453,6 +456,7 @@ fn normalize_under_binder() { } yields { "Ambiguous" } + */ goal { exists { @@ -464,6 +468,7 @@ fn normalize_under_binder() { "Unique; substitution [?0 := I32], lifetime constraints []" } + /* TODO: this doesn't seem to be correct, actually goal { forall<'a> { exists { @@ -473,6 +478,7 @@ fn normalize_under_binder() { } yields { "Ambiguous" } + */ goal { forall<'a> { From 64c9215fe505a1ac7e823201a691e1b4b39137ba Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 17 Mar 2020 15:27:47 +0100 Subject: [PATCH 14/50] Disable currently non-existent caching --- chalk-solve/src/solve.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 970728b1bf1..15ce0fa795a 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -208,7 +208,7 @@ impl SolverChoice { pub fn recursive() -> Self { SolverChoice::Recursive { overflow_depth: 100, - caching_enabled: true, + caching_enabled: false, } } From 9ee81786ad6970e0ff70456c63e896b636e95706 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 17 Mar 2020 17:14:21 +0100 Subject: [PATCH 15/50] Check for input equality --- chalk-ir/src/lib.rs | 9 ++++ chalk-solve/src/recursive/mod.rs | 71 +++++++++++++++++++++++++------- 2 files changed, 65 insertions(+), 15 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index fb4b5eaae12..7f827eaf193 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -1106,6 +1106,15 @@ impl DomainGoal { goal => goal, } } + + pub fn inputs(&self, interner: &I) -> Vec> { + match self { + DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => { + vec![ParameterKind::Ty(alias_eq.alias.clone().intern(interner)).intern()] + } + _ => Vec::new(), + } + } } #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit)] diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 0d1b732c34e..ea0220e45b6 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -353,25 +353,28 @@ impl<'me, I: Interner> Solver<'me, I> { fn combine_with_priorities( a: Solution, prio_a: ClausePriority, + inputs_a: Vec>, b: Solution, prio_b: ClausePriority, - ) -> (Solution, ClausePriority) { + inputs_b: Vec>, + ) -> (Solution, ClausePriority, Vec>) { match (prio_a, prio_b) { - (ClausePriority::High, ClausePriority::Low) => { + // TODO compare the *input* parts of the solutions + (ClausePriority::High, ClausePriority::Low) if inputs_a == inputs_b => { debug!( "preferring solution: {:?} over {:?} because of higher prio", a, b ); - (a, ClausePriority::High) + (a, ClausePriority::High, inputs_a) } - (ClausePriority::Low, ClausePriority::High) => { + (ClausePriority::Low, ClausePriority::High) if inputs_a == inputs_b => { debug!( "preferring solution: {:?} over {:?} because of higher prio", b, a ); - (b, ClausePriority::High) + (b, ClausePriority::High, inputs_b) } - _ => (a.combine(b), prio_a), + _ => (a.combine(b), prio_a, inputs_a), } } for program_clause in clauses { @@ -390,11 +393,30 @@ impl<'me, I: Interner> Solver<'me, I> { ); if let Ok(solution) = res { debug!("ok: solution={:?} prio={:?}", solution, priority); + let inputs = if let Some(subst) = solution.constrained_subst() { + let subst_goal = subst.value.subst.apply( + &canonical_goal.canonical.value.goal, + self.program.interner(), + ); + debug!("subst_goal = {:?}", subst_goal); + subst_goal.inputs(self.program.interner()) + } else { + canonical_goal + .canonical + .value + .goal + .inputs(self.program.interner()) + }; cur_solution = Some(match cur_solution { - None => (solution, priority), - Some((cur, cur_priority)) => { - combine_with_priorities(cur, cur_priority, solution, priority) - } + None => (solution, priority, inputs), + Some((cur, cur_priority, cur_inputs)) => combine_with_priorities( + cur, + cur_priority, + cur_inputs, + solution, + priority, + inputs, + ), }); } else { debug!("error"); @@ -405,11 +427,30 @@ impl<'me, I: Interner> Solver<'me, I> { let res = self.solve_via_implication(canonical_goal, implication, minimums); if let Ok(solution) = res { debug!("ok: solution={:?} prio={:?}", solution, priority); + let inputs = if let Some(subst) = solution.constrained_subst() { + let subst_goal = subst.value.subst.apply( + &canonical_goal.canonical.value.goal, + self.program.interner(), + ); + debug!("subst_goal = {:?}", subst_goal); + subst_goal.inputs(self.program.interner()) + } else { + canonical_goal + .canonical + .value + .goal + .inputs(self.program.interner()) + }; cur_solution = Some(match cur_solution { - None => (solution, priority), - Some((cur, cur_priority)) => { - combine_with_priorities(cur, cur_priority, solution, priority) - } + None => (solution, priority, inputs), + Some((cur, cur_priority, cur_inputs)) => combine_with_priorities( + cur, + cur_priority, + cur_inputs, + solution, + priority, + inputs, + ), }); } else { debug!("error"); @@ -417,7 +458,7 @@ impl<'me, I: Interner> Solver<'me, I> { } } } - cur_solution.map(|(s, _)| s).ok_or(NoSolution) + cur_solution.map(|(s, _, _)| s).ok_or(NoSolution) } /// Modus ponens! That is: try to apply an implication by proving its premises. From 27bc264c1419d51c2194e54f5a78c4fa29c78273 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 17 Mar 2020 17:14:40 +0100 Subject: [PATCH 16/50] Ignore tests currently overflowing/infinitely looping (REMOVE AGAIN) --- tests/test/cycle.rs | 1 + tests/test/misc.rs | 3 +++ tests/test/wf_lowering.rs | 2 ++ 3 files changed, 6 insertions(+) diff --git a/tests/test/cycle.rs b/tests/test/cycle.rs index 4a8fa06cfc4..d5d1f594dfb 100644 --- a/tests/test/cycle.rs +++ b/tests/test/cycle.rs @@ -146,6 +146,7 @@ fn multiple_ambiguous_cycles() { } } +#[ignore] #[test] fn overflow() { test! { diff --git a/tests/test/misc.rs b/tests/test/misc.rs index a3d76bf00f7..265d3aba9df 100644 --- a/tests/test/misc.rs +++ b/tests/test/misc.rs @@ -61,6 +61,7 @@ fn basic() { /// Make sure we don't get a stack overflow or other badness for this /// test from scalexm. +#[ignore] #[test] fn subgoal_abstraction() { test! { @@ -159,6 +160,7 @@ fn only_draw_so_many_blow_up() { } } +#[ignore] #[test] fn subgoal_cycle_uninhabited() { test! { @@ -216,6 +218,7 @@ fn subgoal_cycle_uninhabited() { } } +#[ignore] #[test] fn subgoal_cycle_inhabited() { test! { diff --git a/tests/test/wf_lowering.rs b/tests/test/wf_lowering.rs index 235ae2090b3..48e871bb21f 100644 --- a/tests/test/wf_lowering.rs +++ b/tests/test/wf_lowering.rs @@ -481,6 +481,7 @@ fn higher_ranked_trait_bound_on_gat() { } // See `cyclic_traits`, this is essentially the same but with higher-ranked co-inductive WF goals. +#[ignore] #[test] fn higher_ranked_cyclic_requirements() { lowering_success! { @@ -562,6 +563,7 @@ fn higher_ranked_inline_bound_on_gat() { } } +#[ignore] #[test] fn assoc_type_recursive_bound() { lowering_error! { From 47a473cf1f96f96bdf9acc7e49d0621ffb8d7c7a Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 17 Mar 2020 17:15:56 +0100 Subject: [PATCH 17/50] Projection equality test is fixed --- tests/test/projection.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/tests/test/projection.rs b/tests/test/projection.rs index fcf09a36388..0ba69b8e200 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -143,10 +143,7 @@ fn projection_equality() { S: Trait2 } } yields { - // FIXME(rust-lang/chalk#234) -- there is really only one - // *reasonable* solution here, which is `u32`, but we get - // confused because `(Trait1::Type)` seems valid too. - "Ambiguous; no inference guidance" + "Unique; substitution [?0 := u32]" } } } From 9c27db680c637d646bca293b9645c6d1d981891a Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 17 Mar 2020 17:31:37 +0100 Subject: [PATCH 18/50] Sort constraints in tests The actual order of the constraints doesn't matter, I think; and the recursive solver puts them into a HashSet, so the order may vary. --- tests/test/mod.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/tests/test/mod.rs b/tests/test/mod.rs index 52fcddd8487..dc44a12fa86 100644 --- a/tests/test/mod.rs +++ b/tests/test/mod.rs @@ -14,7 +14,17 @@ mod bench; mod coherence; mod wf_lowering; -fn assert_result(result: &Option>, expected: &str) { +fn assert_result(mut result: Option>, expected: &str) { + // sort constraints, since the different solvers may output them in different order + match &mut result { + Some(Solution::Unique(solution)) => { + solution + .value + .constraints + .sort_by_key(|c| format!("{:?}", c)); + } + _ => {} + } let result = match result { Some(v) => format!("{}", v), None => format!("No possible solution"), @@ -231,7 +241,7 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>) { match expected { TestGoal::Aggregated(expected) => { let result = db.solve(&peeled_goal); - assert_result(&result, expected); + assert_result(result, expected); } TestGoal::All(expected) => { let mut expected = expected.into_iter(); From fa6dd0110bd053539c7b0192ccacf3cce2c9bf5e Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Wed, 18 Mar 2020 13:07:24 +0100 Subject: [PATCH 19/50] Implement floundering for too-general goals, like the SLG solver --- chalk-solve/src/recursive/mod.rs | 52 +++++++++++++++++++++++++++++--- chalk-solve/src/solve/slg.rs | 1 + 2 files changed, 48 insertions(+), 5 deletions(-) diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index ea0220e45b6..43eba1b76a4 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -7,7 +7,10 @@ mod stack; use self::fulfill::Fulfill; use self::search_graph::{DepthFirstNumber, SearchGraph}; use self::stack::{Stack, StackDepth}; -use chalk_engine::fallible::{Fallible, NoSolution}; +use chalk_engine::{ + context::Floundered, + fallible::{Fallible, NoSolution}, +}; use chalk_ir::could_match::CouldMatch; use clauses::program_clauses_for_goal; @@ -258,10 +261,13 @@ impl<'me, I: Interner> Solver<'me, I> { let prog_solution = { debug_heading!("prog_clauses"); - // TODO this also includes clauses from env - let prog_clauses = - program_clauses_for_goal(self.program, environment, &goal); - self.solve_from_clauses(&canonical_goal, prog_clauses, minimums) + let prog_clauses = self.program_clauses_for_goal(environment, &goal); + prog_clauses.map_or( + Ok(Solution::Ambig(Guidance::Unknown)), + |prog_clauses| { + self.solve_from_clauses(&canonical_goal, prog_clauses, minimums) + }, + ) }; debug!("prog_solution={:?}", prog_solution); @@ -272,6 +278,7 @@ impl<'me, I: Interner> Solver<'me, I> { // inference. The idea is that the assumptions you've explicitly // made in a given context are more likely to be relevant than // general `impl`s. + // TODO can we combine this logic with the priorization logic? env_solution.merge_with(prog_solution, |env, prog| env.favor_over(prog)) } @@ -494,6 +501,41 @@ impl<'me, I: Interner> Solver<'me, I> { // and then try to solve fulfill.solve(subst, minimums) } + + fn program_clauses_for_goal( + &self, + environment: &Environment, + goal: &DomainGoal, + ) -> Result>, Floundered> { + // TODO this is currently duplicated with the SLG solver, extract it somewhere? + // Look for floundering goals: + match goal { + // Check for a goal like `?T: Foo` where `Foo` is not enumerable. + DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => { + let trait_datum = self.program.trait_datum(trait_ref.trait_id); + if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() { + let self_ty = trait_ref.self_type_parameter(); + if let Some(_) = self_ty.bound() { + return Err(Floundered); + } + } + } + + DomainGoal::WellFormed(WellFormed::Ty(ty)) + | DomainGoal::IsUpstream(ty) + | DomainGoal::DownstreamType(ty) + | DomainGoal::IsFullyVisible(ty) + | DomainGoal::IsLocal(ty) => match ty.data() { + TyData::BoundVar(_) => return Err(Floundered), + _ => {} + }, + + _ => {} + } + + // TODO this also includes clauses from env + Ok(program_clauses_for_goal(self.program, environment, goal)) + } } impl Minimums { diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs index 7be415a1d13..35e4aebb747 100644 --- a/chalk-solve/src/solve/slg.rs +++ b/chalk-solve/src/solve/slg.rs @@ -207,6 +207,7 @@ impl<'me, I: Interner> context::ContextOps> for SlgContextOps<'me, let mut clauses: Vec<_> = program_clauses_for_goal(self.program, environment, goal); + // TODO this is redundant, I think clauses.extend( environment .clauses From a81d3456803fe384279d58e7e70bf8ca9a5fdecf Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Wed, 18 Mar 2020 13:34:26 +0100 Subject: [PATCH 20/50] Truncate goals like in the SLG solver --- chalk-solve/src/recursive/fulfill.rs | 6 +++++- chalk-solve/src/recursive/mod.rs | 4 ++-- chalk-solve/src/solve.rs | 2 +- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index f735de7d92b..fe162b0a112 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -1,4 +1,5 @@ use super::*; +use crate::solve::truncate; use cast::Caster; use chalk_engine::fallible::NoSolution; use fold::Fold; @@ -191,11 +192,14 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { minimums: &mut Minimums, ) -> Fallible> { let interner = self.solver.program.interner(); + // truncate to avoid overflows + let truncated = + truncate::truncate(self.solver.program.interner(), &mut self.infer, 10, &wc); let Canonicalized { quantified, free_vars, .. - } = self.infer.canonicalize(interner, wc); + } = self.infer.canonicalize(interner, &truncated.value); let UCanonicalized { quantified, universes, diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 43eba1b76a4..bac44312bfa 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -151,7 +151,7 @@ impl<'me, I: Interner> Solver<'me, I> { // Return the solution from the table. let previous_solution = self.context.search_graph[dfn].solution.clone(); - debug!( + info!( "solve_goal: cycle detected, previous solution {:?}", previous_solution ); @@ -187,7 +187,7 @@ impl<'me, I: Interner> Solver<'me, I> { } } - debug!("solve_goal: solution = {:?}", result,); + info!("solve_goal: solution = {:?}", result,); result } } diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 15ce0fa795a..681d42f053a 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -6,7 +6,7 @@ use chalk_ir::*; use std::fmt; mod slg; -mod truncate; +pub(crate) mod truncate; /// A (possible) solution for a proposed goal. #[derive(Clone, Debug, PartialEq, Eq)] From d8ed6292c389cd0d680b19d319d814591a097899 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Wed, 18 Mar 2020 13:34:49 +0100 Subject: [PATCH 21/50] Revert "Ignore tests currently overflowing/infinitely looping (REMOVE AGAIN)" This reverts commit 66332f8bab83b49577bb26311a6579e2d71b8b71. --- tests/test/cycle.rs | 1 - tests/test/misc.rs | 3 --- tests/test/wf_lowering.rs | 2 -- 3 files changed, 6 deletions(-) diff --git a/tests/test/cycle.rs b/tests/test/cycle.rs index d5d1f594dfb..4a8fa06cfc4 100644 --- a/tests/test/cycle.rs +++ b/tests/test/cycle.rs @@ -146,7 +146,6 @@ fn multiple_ambiguous_cycles() { } } -#[ignore] #[test] fn overflow() { test! { diff --git a/tests/test/misc.rs b/tests/test/misc.rs index 265d3aba9df..a3d76bf00f7 100644 --- a/tests/test/misc.rs +++ b/tests/test/misc.rs @@ -61,7 +61,6 @@ fn basic() { /// Make sure we don't get a stack overflow or other badness for this /// test from scalexm. -#[ignore] #[test] fn subgoal_abstraction() { test! { @@ -160,7 +159,6 @@ fn only_draw_so_many_blow_up() { } } -#[ignore] #[test] fn subgoal_cycle_uninhabited() { test! { @@ -218,7 +216,6 @@ fn subgoal_cycle_uninhabited() { } } -#[ignore] #[test] fn subgoal_cycle_inhabited() { test! { diff --git a/tests/test/wf_lowering.rs b/tests/test/wf_lowering.rs index 48e871bb21f..235ae2090b3 100644 --- a/tests/test/wf_lowering.rs +++ b/tests/test/wf_lowering.rs @@ -481,7 +481,6 @@ fn higher_ranked_trait_bound_on_gat() { } // See `cyclic_traits`, this is essentially the same but with higher-ranked co-inductive WF goals. -#[ignore] #[test] fn higher_ranked_cyclic_requirements() { lowering_success! { @@ -563,7 +562,6 @@ fn higher_ranked_inline_bound_on_gat() { } } -#[ignore] #[test] fn assoc_type_recursive_bound() { lowering_error! { From 3e8c1ae2095bf35138d6bbcca6800a74e1d25d99 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 22 Mar 2020 12:52:22 +0100 Subject: [PATCH 22/50] Add back the old caching for now --- chalk-solve/src/recursive/mod.rs | 17 ++++++++++------- chalk-solve/src/recursive/search_graph.rs | 3 ++- chalk-solve/src/solve.rs | 2 +- 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index bac44312bfa..6ff04196f47 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -13,12 +13,14 @@ use chalk_engine::{ }; use chalk_ir::could_match::CouldMatch; use clauses::program_clauses_for_goal; +use rustc_hash::FxHashMap; type UCanonicalGoal = UCanonical>>; pub(crate) struct RecursiveContext { stack: Stack, search_graph: SearchGraph, + cache: FxHashMap, Fallible>>, caching_enabled: bool, } @@ -65,6 +67,7 @@ impl RecursiveContext { RecursiveContext { stack: Stack::new(overflow_depth), search_graph: SearchGraph::new(), + cache: FxHashMap::default(), caching_enabled, } } @@ -117,11 +120,10 @@ impl<'me, I: Interner> Solver<'me, I> { info_heading!("solve_goal({:?})", goal); // First check the cache. - // TODO - // if let Some(value) = self.cache.get(&goal) { - // debug!("solve_reduced_goal: cache hit, value={:?}", value); - // return value.clone(); - // } + if let Some(value) = self.context.cache.get(&goal) { + debug!("solve_reduced_goal: cache hit, value={:?}", value); + return value.clone(); + } // Next, check if the goal is in the search tree already. if let Some(dfn) = self.context.search_graph.lookup(&goal) { @@ -176,8 +178,9 @@ impl<'me, I: Interner> Solver<'me, I> { // worst of the repeated work that we do during tabling. if subgoal_minimums.positive >= dfn { if self.context.caching_enabled { - // TODO - // self.search_graph.move_to_cache(dfn, &mut self.cache); + self.context + .search_graph + .move_to_cache(dfn, &mut self.context.cache); debug!("solve_reduced_goal: SCC head encountered, moving to cache"); } else { debug!( diff --git a/chalk-solve/src/recursive/search_graph.rs b/chalk-solve/src/recursive/search_graph.rs index 26f17ca3ac2..da61a8093f3 100644 --- a/chalk-solve/src/recursive/search_graph.rs +++ b/chalk-solve/src/recursive/search_graph.rs @@ -9,6 +9,7 @@ use super::{Minimums, UCanonicalGoal}; use crate::Solution; use chalk_engine::fallible::{Fallible, NoSolution}; use chalk_ir::interner::Interner; +use rustc_hash::FxHashMap; pub(super) struct SearchGraph { indices: HashMap, DepthFirstNumber>, @@ -86,7 +87,7 @@ impl SearchGraph { pub(crate) fn move_to_cache( &mut self, dfn: DepthFirstNumber, - cache: &mut HashMap, Fallible>>, + cache: &mut FxHashMap, Fallible>>, ) { debug!("move_to_cache(dfn={:?})", dfn); self.indices.retain(|_key, value| *value < dfn); diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index 681d42f053a..ad2652f878f 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -208,7 +208,7 @@ impl SolverChoice { pub fn recursive() -> Self { SolverChoice::Recursive { overflow_depth: 100, - caching_enabled: false, + caching_enabled: true, } } From de95b375aee27b83c489cf9ce23d905646a0d0e1 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 22 Mar 2020 13:39:52 +0100 Subject: [PATCH 23/50] Keep track of clause priority for longer to avoid infinite loop --- chalk-ir/src/lib.rs | 10 +++ chalk-solve/src/recursive/fulfill.rs | 33 +++++-- chalk-solve/src/recursive/mod.rs | 101 ++++++++++++++-------- chalk-solve/src/recursive/search_graph.rs | 4 +- 4 files changed, 102 insertions(+), 46 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 7f827eaf193..c75676f0947 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -1322,6 +1322,16 @@ pub enum ClausePriority { Low, } +impl std::ops::BitAnd for ClausePriority { + type Output = ClausePriority; + fn bitand(self, rhs: ClausePriority) -> Self::Output { + match (self, rhs) { + (ClausePriority::High, ClausePriority::High) => ClausePriority::High, + _ => ClausePriority::Low, + } + } +} + #[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner)] pub enum ProgramClauseData { Implies(ProgramClauseImplication), diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index fe162b0a112..aa980c3737f 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -75,6 +75,8 @@ pub(crate) struct Fulfill<'s, 'db, I: Interner> { /// The remaining goals to prove or refute obligations: Vec>, + priority: ClausePriority, + /// Lifetime constraints that must be fulfilled for a solution to be fully /// validated. constraints: HashSet>>, @@ -89,6 +91,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { pub(crate) fn new + HasInterner + Clone>( solver: &'s mut Solver<'db, I>, ucanonical_goal: &UCanonical>, + priority: ClausePriority, ) -> (Self, Substitution, InEnvironment) { let (infer, subst, canonical_goal) = InferenceTable::from_canonical( solver.program.interner(), @@ -99,6 +102,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { solver, infer, obligations: vec![], + priority, constraints: HashSet::new(), cannot_prove: false, }; @@ -204,10 +208,12 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { quantified, universes, } = self.infer.u_canonicalize(interner, &quantified); + let (result, new_priority) = self.solver.solve_goal(quantified, minimums); + self.priority = self.priority & new_priority; Ok(PositiveSolution { free_vars, universes, - solution: self.solver.solve_goal(quantified, minimums)?, + solution: result?, }) } @@ -232,7 +238,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { .infer .u_canonicalize(self.solver.program.interner(), &canonicalized); let mut minimums = Minimums::new(); // FIXME -- minimums here seems wrong - if let Ok(solution) = self.solver.solve_goal(quantified, &mut minimums) { + if let (Ok(solution), _priority) = self.solver.solve_goal(quantified, &mut minimums) { if solution.is_unique() { Err(NoSolution) } else { @@ -361,11 +367,14 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { mut self, subst: Substitution, minimums: &mut Minimums, - ) -> Fallible> { - let outcome = self.fulfill(minimums)?; + ) -> (Fallible>, ClausePriority) { + let outcome = match self.fulfill(minimums) { + Ok(o) => o, + Err(e) => return (Err(e), self.priority), + }; if self.cannot_prove { - return Ok(Solution::Ambig(Guidance::Unknown)); + return (Ok(Solution::Ambig(Guidance::Unknown)), self.priority); } if outcome.is_complete() { @@ -377,7 +386,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { self.solver.program.interner(), &ConstrainedSubst { subst, constraints }, ); - return Ok(Solution::Unique(constrained.quantified)); + return (Ok(Solution::Unique(constrained.quantified)), self.priority); } // Otherwise, we have (positive or negative) obligations remaining, but @@ -405,12 +414,15 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let subst = self .infer .canonicalize(self.solver.program.interner(), &subst); - return Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))); + return ( + Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))), + self.priority, + ); } } } - Ok(Solution::Ambig(Guidance::Unknown)) + (Ok(Solution::Ambig(Guidance::Unknown)), self.priority) } else { // While we failed to prove the goal, we still learned that // something had to hold. Here's an example where this happens: @@ -435,7 +447,10 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let subst = self .infer .canonicalize(self.solver.program.interner(), &subst); - Ok(Solution::Ambig(Guidance::Definite(subst.quantified))) + ( + Ok(Solution::Ambig(Guidance::Definite(subst.quantified))), + self.priority, + ) } } diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 6ff04196f47..c86d7f95d24 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -106,7 +106,7 @@ impl<'me, I: Interner> Solver<'me, I> { debug!("solve_root_goal(canonical_goal={:?})", canonical_goal); assert!(self.context.stack.is_empty()); let minimums = &mut Minimums::new(); - self.solve_goal(canonical_goal.clone(), minimums) + self.solve_goal(canonical_goal.clone(), minimums).0 } /// Attempt to solve a goal that has been fully broken down into leaf form @@ -116,13 +116,13 @@ impl<'me, I: Interner> Solver<'me, I> { &mut self, goal: UCanonicalGoal, minimums: &mut Minimums, - ) -> Fallible> { + ) -> (Fallible>, ClausePriority) { info_heading!("solve_goal({:?})", goal); // First check the cache. if let Some(value) = self.context.cache.get(&goal) { debug!("solve_reduced_goal: cache hit, value={:?}", value); - return value.clone(); + return (value.clone(), ClausePriority::High); } // Next, check if the goal is in the search tree already. @@ -140,10 +140,13 @@ impl<'me, I: Interner> Solver<'me, I> { constraints: vec![], }; debug!("applying coinductive semantics"); - return Ok(Solution::Unique(Canonical { - value, - binders: goal.canonical.binders, - })); + return ( + Ok(Solution::Unique(Canonical { + value, + binders: goal.canonical.binders, + })), + ClausePriority::High, + ); } self.context.stack[depth].flag_cycle(); @@ -153,11 +156,12 @@ impl<'me, I: Interner> Solver<'me, I> { // Return the solution from the table. let previous_solution = self.context.search_graph[dfn].solution.clone(); + let previous_solution_priority = self.context.search_graph[dfn].solution_priority; info!( - "solve_goal: cycle detected, previous solution {:?}", - previous_solution + "solve_goal: cycle detected, previous solution {:?} with prio {:?}", + previous_solution, previous_solution_priority ); - previous_solution + (previous_solution, previous_solution_priority) } else { // Otherwise, push the goal onto the stack and create a table. // The initial result for this table is error. @@ -171,6 +175,7 @@ impl<'me, I: Interner> Solver<'me, I> { // Read final result from table. let result = self.context.search_graph[dfn].solution.clone(); + let priority = self.context.search_graph[dfn].solution_priority; // If processing this subgoal did not involve anything // outside of its subtree, then we can promote it to the @@ -190,8 +195,8 @@ impl<'me, I: Interner> Solver<'me, I> { } } - info!("solve_goal: solution = {:?}", result,); - result + info!("solve_goal: solution = {:?} prio {:?}", result, priority); + (result, priority) } } @@ -228,7 +233,7 @@ impl<'me, I: Interner> Solver<'me, I> { }, } = canonical_goal.clone(); - let current_answer = match goal.data() { + let (current_answer, current_prio) = match goal.data() { GoalData::DomainGoal(domain_goal) => { let canonical_goal = UCanonical { universes, @@ -248,7 +253,7 @@ impl<'me, I: Interner> Solver<'me, I> { // clauses. We try each approach in turn: let InEnvironment { environment, goal } = &canonical_goal.canonical.value; - let env_solution = { + let (env_solution, env_prio) = { debug_heading!("env_clauses"); // TODO use code from clauses module @@ -261,16 +266,18 @@ impl<'me, I: Interner> Solver<'me, I> { }; debug!("env_solution={:?}", env_solution); - let prog_solution = { + let (prog_solution, prog_prio) = { debug_heading!("prog_clauses"); let prog_clauses = self.program_clauses_for_goal(environment, &goal); - prog_clauses.map_or( - Ok(Solution::Ambig(Guidance::Unknown)), - |prog_clauses| { - self.solve_from_clauses(&canonical_goal, prog_clauses, minimums) - }, - ) + match prog_clauses { + Ok(clauses) => { + self.solve_from_clauses(&canonical_goal, clauses, minimums) + } + Err(Floundered) => { + (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High) + } + } }; debug!("prog_solution={:?}", prog_solution); @@ -282,7 +289,10 @@ impl<'me, I: Interner> Solver<'me, I> { // made in a given context are more likely to be relevant than // general `impl`s. // TODO can we combine this logic with the priorization logic? - env_solution.merge_with(prog_solution, |env, prog| env.favor_over(prog)) + ( + env_solution.merge_with(prog_solution, |env, prog| env.favor_over(prog)), + prog_prio & env_prio, // FIXME + ) } _ => { @@ -307,6 +317,7 @@ impl<'me, I: Interner> Solver<'me, I> { // None of our subgoals depended on us directly. // We can return. self.context.search_graph[dfn].solution = current_answer; + self.context.search_graph[dfn].solution_priority = current_prio; return *minimums; } @@ -317,12 +328,24 @@ impl<'me, I: Interner> Solver<'me, I> { return *minimums; } + if ( + self.context.search_graph[dfn].solution_priority, + current_prio, + ) == (ClausePriority::High, ClausePriority::Low) + { + // TODO check solution inputs? + // Not replacing the current answer, so we're at a fixed point? + debug!("solve_new_subgoal: new answer has lower priority"); + return *minimums; + } + let current_answer_is_ambig = match ¤t_answer { Ok(s) => s.is_ambig(), Err(_) => false, }; self.context.search_graph[dfn].solution = current_answer; + self.context.search_graph[dfn].solution_priority = current_prio; // Subtle: if our current answer is ambiguous, we can just stop, and // in fact we *must* -- otherwise, we sometimes fail to reach a @@ -340,10 +363,12 @@ impl<'me, I: Interner> Solver<'me, I> { &mut self, canonical_goal: &UCanonicalGoal, minimums: &mut Minimums, - ) -> Fallible> { + ) -> (Fallible>, ClausePriority) { debug_heading!("solve_via_simplification({:?})", canonical_goal); - let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal); - fulfill.push_goal(&goal.environment, goal.goal)?; + let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal, ClausePriority::High); + if let Err(e) = fulfill.push_goal(&goal.environment, goal.goal) { + return (Err(e), ClausePriority::High); + } fulfill.solve(subst, minimums) } @@ -355,10 +380,11 @@ impl<'me, I: Interner> Solver<'me, I> { canonical_goal: &UCanonical>>, clauses: C, minimums: &mut Minimums, - ) -> Fallible> + ) -> (Fallible>, ClausePriority) where C: IntoIterator>, { + // TODO we don't actually need to keep track of the inputs let mut cur_solution = None; fn combine_with_priorities( a: Solution, @@ -369,7 +395,6 @@ impl<'me, I: Interner> Solver<'me, I> { inputs_b: Vec>, ) -> (Solution, ClausePriority, Vec>) { match (prio_a, prio_b) { - // TODO compare the *input* parts of the solutions (ClausePriority::High, ClausePriority::Low) if inputs_a == inputs_b => { debug!( "preferring solution: {:?} over {:?} because of higher prio", @@ -392,7 +417,6 @@ impl<'me, I: Interner> Solver<'me, I> { match program_clause { ProgramClause::Implies(implication) => { - let priority = implication.priority; let res = self.solve_via_implication( canonical_goal, Binders { @@ -401,7 +425,7 @@ impl<'me, I: Interner> Solver<'me, I> { }, minimums, ); - if let Ok(solution) = res { + if let (Ok(solution), priority) = res { debug!("ok: solution={:?} prio={:?}", solution, priority); let inputs = if let Some(subst) = solution.constrained_subst() { let subst_goal = subst.value.subst.apply( @@ -433,9 +457,8 @@ impl<'me, I: Interner> Solver<'me, I> { } } ProgramClause::ForAll(implication) => { - let priority = implication.value.priority; let res = self.solve_via_implication(canonical_goal, implication, minimums); - if let Ok(solution) = res { + if let (Ok(solution), priority) = res { debug!("ok: solution={:?} prio={:?}", solution, priority); let inputs = if let Some(subst) = solution.constrained_subst() { let subst_goal = subst.value.subst.apply( @@ -468,7 +491,9 @@ impl<'me, I: Interner> Solver<'me, I> { } } } - cur_solution.map(|(s, _, _)| s).ok_or(NoSolution) + cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p, _)| { + (Ok(s), p) + }) } /// Modus ponens! That is: try to apply an implication by proving its premises. @@ -477,7 +502,7 @@ impl<'me, I: Interner> Solver<'me, I> { canonical_goal: &UCanonical>>, clause: Binders>, minimums: &mut Minimums, - ) -> Fallible> { + ) -> (Fallible>, ClausePriority) { info_heading!( "solve_via_implication(\ \n canonical_goal={:?},\ @@ -485,7 +510,7 @@ impl<'me, I: Interner> Solver<'me, I> { canonical_goal, clause ); - let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal); + let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal, clause.value.priority); let ProgramClauseImplication { consequence, conditions, @@ -494,11 +519,15 @@ impl<'me, I: Interner> Solver<'me, I> { debug!("the subst is {:?}", subst); - fulfill.unify(&goal.environment, &goal.goal, &consequence)?; + if let Err(e) = fulfill.unify(&goal.environment, &goal.goal, &consequence) { + return (Err(e), ClausePriority::High); + } // if so, toss in all of its premises for condition in conditions.as_slice() { - fulfill.push_goal(&goal.environment, condition.clone())?; + if let Err(e) = fulfill.push_goal(&goal.environment, condition.clone()) { + return (Err(e), ClausePriority::High); + } } // and then try to solve diff --git a/chalk-solve/src/recursive/search_graph.rs b/chalk-solve/src/recursive/search_graph.rs index da61a8093f3..418780c3c7d 100644 --- a/chalk-solve/src/recursive/search_graph.rs +++ b/chalk-solve/src/recursive/search_graph.rs @@ -8,7 +8,7 @@ use super::stack::StackDepth; use super::{Minimums, UCanonicalGoal}; use crate::Solution; use chalk_engine::fallible::{Fallible, NoSolution}; -use chalk_ir::interner::Interner; +use chalk_ir::{interner::Interner, ClausePriority}; use rustc_hash::FxHashMap; pub(super) struct SearchGraph { @@ -25,6 +25,7 @@ pub(super) struct Node { pub(crate) goal: UCanonicalGoal, pub(crate) solution: Fallible>, + pub(crate) solution_priority: ClausePriority, /// This is `Some(X)` if we are actively exploring this node, or /// `None` otherwise. @@ -66,6 +67,7 @@ impl SearchGraph { let node = Node { goal: goal.clone(), solution: Err(NoSolution), + solution_priority: ClausePriority::High, stack_depth: Some(stack_depth), links: Minimums { positive: dfn }, }; From 9ab02e2577d63ee52b5aeb3faf1f0d1352eed34c Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 24 Mar 2020 22:09:25 +0100 Subject: [PATCH 24/50] Flounder for AliasEq with unspecific self type as well --- chalk-ir/src/lib.rs | 8 ++++++++ chalk-solve/src/recursive/mod.rs | 7 +++++++ 2 files changed, 15 insertions(+) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index c75676f0947..37671d82104 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -839,6 +839,14 @@ impl AliasTy { pub fn intern(self, interner: &I) -> Ty { Ty::new(interner, self) } + + pub fn type_parameters<'a>(&'a self) -> impl Iterator> + 'a { + self.substitution.iter().filter_map(|p| p.ty()).cloned() + } + + pub fn self_type_parameter(&self) -> Ty { + self.type_parameters().next().unwrap() + } } #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index c86d7f95d24..4fbd1a7c499 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -553,6 +553,13 @@ impl<'me, I: Interner> Solver<'me, I> { } } + DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => { + let self_ty = alias_eq.alias.self_type_parameter(); + if let Some(_) = self_ty.bound() { + return Err(Floundered); + } + } + DomainGoal::WellFormed(WellFormed::Ty(ty)) | DomainGoal::IsUpstream(ty) | DomainGoal::DownstreamType(ty) From e661d850bb07824831d5640548f01062c81ea6dc Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Fri, 27 Mar 2020 15:42:04 +0100 Subject: [PATCH 25/50] Rebase fixes --- chalk-ir/src/lib.rs | 18 +++++++++++------- chalk-solve/src/clauses.rs | 10 +++++----- chalk-solve/src/infer.rs | 14 +++++++++----- chalk-solve/src/recursive/fulfill.rs | 19 +++++++++++++------ chalk-solve/src/recursive/mod.rs | 23 +++++++++++++---------- 5 files changed, 51 insertions(+), 33 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 37671d82104..917aedfa82a 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -840,12 +840,15 @@ impl AliasTy { Ty::new(interner, self) } - pub fn type_parameters<'a>(&'a self) -> impl Iterator> + 'a { - self.substitution.iter().filter_map(|p| p.ty()).cloned() + pub fn type_parameters<'a>(&'a self, interner: &'a I) -> impl Iterator> + 'a { + self.substitution + .iter(interner) + .filter_map(move |p| p.ty(interner)) + .cloned() } - pub fn self_type_parameter(&self) -> Ty { - self.type_parameters().next().unwrap() + pub fn self_type_parameter(&self, interner: &I) -> Ty { + self.type_parameters(interner).next().unwrap() } } @@ -1118,7 +1121,7 @@ impl DomainGoal { pub fn inputs(&self, interner: &I) -> Vec> { match self { DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => { - vec![ParameterKind::Ty(alias_eq.alias.clone().intern(interner)).intern()] + vec![ParameterKind::Ty(alias_eq.alias.clone().intern(interner)).intern(interner)] } _ => Vec::new(), } @@ -1505,16 +1508,17 @@ impl UCanonical { pub fn trivial_substitution(&self, interner: &I) -> Substitution { let binders = &self.canonical.binders; Substitution::from( + interner, binders .iter() .enumerate() .map(|(index, pk)| match pk { ParameterKind::Ty(_) => { - ParameterKind::Ty(TyData::BoundVar(index).intern(interner)).intern() + ParameterKind::Ty(TyData::BoundVar(index).intern(interner)).intern(interner) } ParameterKind::Lifetime(_) => { ParameterKind::Lifetime(LifetimeData::BoundVar(index).intern(interner)) - .intern() + .intern(interner) } }) .collect::>(), diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 01ad3ad4f3d..943612e89e9 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -452,8 +452,8 @@ mod generalize { } } - impl Folder for Generalize<'_, I> { - fn as_dyn(&mut self) -> &mut dyn Folder { + impl<'i, I: Interner> Folder<'i, I> for Generalize<'i, I> { + fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> { self } @@ -481,12 +481,12 @@ mod generalize { Ok(LifetimeData::BoundVar(*new_index + binders).intern(self.interner())) } - fn interner(&self) -> &I { + fn interner(&self) -> &'i I { self.interner } - fn target_interner(&self) -> &I { - self.interner() + fn target_interner(&self) -> &'i I { + self.interner } } } diff --git a/chalk-solve/src/infer.rs b/chalk-solve/src/infer.rs index 5b9af119b68..6176c838a67 100644 --- a/chalk-solve/src/infer.rs +++ b/chalk-solve/src/infer.rs @@ -202,11 +202,15 @@ impl InferenceTable { /// Check whether the given substitution is the identity substitution in this /// inference context. - pub(crate) fn is_trivial_substitution(&mut self, subst: &Substitution) -> bool { - for value in subst.as_parameters() { - match value.data() { + pub(crate) fn is_trivial_substitution( + &mut self, + interner: &I, + subst: &Substitution, + ) -> bool { + for value in subst.as_parameters(interner) { + match value.data(interner) { ParameterKind::Ty(ty) => { - if let Some(var) = ty.inference_var() { + if let Some(var) = ty.inference_var(interner) { if self.var_is_bound(var) { return false; } @@ -214,7 +218,7 @@ impl InferenceTable { } ParameterKind::Lifetime(lifetime) => { - if let Some(var) = lifetime.inference_var() { + if let Some(var) = lifetime.inference_var(interner) { if self.var_is_bound(var) { return false; } diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index aa980c3737f..43c088af904 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -137,8 +137,12 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { debug!("unify: goals={:?}", goals); debug!("unify: constraints={:?}", constraints); self.constraints.extend(constraints); - self.obligations - .extend(goals.into_iter().casted().map(Obligation::Prove)); + self.obligations.extend( + goals + .into_iter() + .casted(self.solver.program.interner()) + .map(Obligation::Prove), + ); Ok(()) } @@ -150,7 +154,8 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { goal: Goal, ) -> Fallible<()> { debug!("push_goal({:?}, {:?})", goal, environment); - match goal.data() { + let interner = self.interner(); + match goal.data(interner) { GoalData::Quantified(QuantifierKind::ForAll, subgoal) => { let subgoal = self .infer @@ -168,7 +173,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { self.push_goal(new_environment, subgoal.clone())?; } GoalData::All(goals) => { - for subgoal in goals.as_slice() { + for subgoal in goals.as_slice(interner) { self.push_goal(environment, subgoal.clone())?; } } @@ -280,7 +285,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let empty_env = &Environment::new(); for (i, free_var) in free_vars.into_iter().enumerate() { - let subst_value = subst.at(i); + let subst_value = subst.at(self.interner(), i); let free_value = free_var.to_parameter(self.interner()); self.unify(empty_env, &free_value, subst_value) .unwrap_or_else(|err| { @@ -394,7 +399,9 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { // need to determine how to package up what we learned about type // inference as an ambiguous solution. - if self.infer.is_trivial_substitution(&subst) { + let interner = self.solver.program.interner(); + + if self.infer.is_trivial_substitution(interner, &subst) { // In this case, we didn't learn *anything* definitively. So now, we // go one last time through the positive obligations, this time // applying even *tentative* inference suggestions, so that we can diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 4fbd1a7c499..ef1062eb42d 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -233,7 +233,7 @@ impl<'me, I: Interner> Solver<'me, I> { }, } = canonical_goal.clone(); - let (current_answer, current_prio) = match goal.data() { + let (current_answer, current_prio) = match goal.data(self.program.interner()) { GoalData::DomainGoal(domain_goal) => { let canonical_goal = UCanonical { universes, @@ -257,11 +257,12 @@ impl<'me, I: Interner> Solver<'me, I> { debug_heading!("env_clauses"); // TODO use code from clauses module - let env_clauses = environment + let env_clauses: Vec<_> = environment .clauses .iter() - .filter(|&clause| clause.could_match(goal)) - .cloned(); + .filter(|&clause| clause.could_match(self.program.interner(), goal)) + .cloned() + .collect(); self.solve_from_clauses(&canonical_goal, env_clauses, minimums) }; debug!("env_solution={:?}", env_solution); @@ -510,6 +511,7 @@ impl<'me, I: Interner> Solver<'me, I> { canonical_goal, clause ); + let interner = self.program.interner(); let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal, clause.value.priority); let ProgramClauseImplication { consequence, @@ -524,7 +526,7 @@ impl<'me, I: Interner> Solver<'me, I> { } // if so, toss in all of its premises - for condition in conditions.as_slice() { + for condition in conditions.as_slice(interner) { if let Err(e) = fulfill.push_goal(&goal.environment, condition.clone()) { return (Err(e), ClausePriority::High); } @@ -541,21 +543,22 @@ impl<'me, I: Interner> Solver<'me, I> { ) -> Result>, Floundered> { // TODO this is currently duplicated with the SLG solver, extract it somewhere? // Look for floundering goals: + let interner = self.program.interner(); match goal { // Check for a goal like `?T: Foo` where `Foo` is not enumerable. DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => { let trait_datum = self.program.trait_datum(trait_ref.trait_id); if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() { - let self_ty = trait_ref.self_type_parameter(); - if let Some(_) = self_ty.bound() { + let self_ty = trait_ref.self_type_parameter(interner); + if let Some(_) = self_ty.bound(interner) { return Err(Floundered); } } } DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => { - let self_ty = alias_eq.alias.self_type_parameter(); - if let Some(_) = self_ty.bound() { + let self_ty = alias_eq.alias.self_type_parameter(interner); + if let Some(_) = self_ty.bound(interner) { return Err(Floundered); } } @@ -564,7 +567,7 @@ impl<'me, I: Interner> Solver<'me, I> { | DomainGoal::IsUpstream(ty) | DomainGoal::DownstreamType(ty) | DomainGoal::IsFullyVisible(ty) - | DomainGoal::IsLocal(ty) => match ty.data() { + | DomainGoal::IsLocal(ty) => match ty.data(interner) { TyData::BoundVar(_) => return Err(Floundered), _ => {} }, From 7e48a62d9c073f14e3a3ece3ff6f85db7b139196 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Fri, 27 Mar 2020 18:52:30 +0100 Subject: [PATCH 26/50] Truncate when adding obligations to avoid messing up the progress assumption ... in the fulfill loop. --- chalk-solve/src/recursive/fulfill.rs | 39 ++++++++++++++++++---------- 1 file changed, 25 insertions(+), 14 deletions(-) diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index 43c088af904..65c332a0a3d 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -1,6 +1,6 @@ use super::*; use crate::solve::truncate; -use cast::Caster; +use cast::Cast; use chalk_engine::fallible::NoSolution; use fold::Fold; use infer::{ @@ -110,7 +110,6 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { } /// Wraps `InferenceTable::instantiate_in` - #[allow(non_camel_case_types)] pub(crate) fn instantiate_binders_existentially( &mut self, arg: impl IntoBindersAndValue, @@ -122,6 +121,23 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { .instantiate_binders_existentially(self.solver.program.interner(), arg) } + fn push_obligation(&mut self, obligation: Obligation) { + // truncate to avoid overflows + let obligation = match obligation { + Obligation::Prove(goal) => { + let truncated = + truncate::truncate(self.solver.program.interner(), &mut self.infer, 10, &goal); + Obligation::Prove(truncated.value) + } + Obligation::Refute(goal) => { + let truncated = + truncate::truncate(self.solver.program.interner(), &mut self.infer, 10, &goal); + Obligation::Refute(truncated.value) + } + }; + self.obligations.push(obligation); + } + /// Unifies `a` and `b` in the given environment. /// /// Wraps `InferenceTable::unify`; any resulting normalizations are added @@ -137,12 +153,10 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { debug!("unify: goals={:?}", goals); debug!("unify: constraints={:?}", constraints); self.constraints.extend(constraints); - self.obligations.extend( - goals - .into_iter() - .casted(self.solver.program.interner()) - .map(Obligation::Prove), - ); + let interner = self.solver.program.interner(); + for goal in goals { + self.push_obligation(Obligation::Prove(goal.cast(interner))); + } Ok(()) } @@ -179,11 +193,11 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { } GoalData::Not(subgoal) => { let in_env = InEnvironment::new(environment, subgoal.clone()); - self.obligations.push(Obligation::Refute(in_env)); + self.push_obligation(Obligation::Refute(in_env)); } GoalData::DomainGoal(_) => { let in_env = InEnvironment::new(environment, goal); - self.obligations.push(Obligation::Prove(in_env)); + self.push_obligation(Obligation::Prove(in_env)); } GoalData::EqGoal(EqGoal { a, b }) => { self.unify(&environment, &a, &b)?; @@ -201,14 +215,11 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { minimums: &mut Minimums, ) -> Fallible> { let interner = self.solver.program.interner(); - // truncate to avoid overflows - let truncated = - truncate::truncate(self.solver.program.interner(), &mut self.infer, 10, &wc); let Canonicalized { quantified, free_vars, .. - } = self.infer.canonicalize(interner, &truncated.value); + } = self.infer.canonicalize(interner, &wc); let UCanonicalized { quantified, universes, From 04b57da29f8599085bb3df24281ec21079b0d0f8 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Mon, 30 Mar 2020 20:30:05 +0200 Subject: [PATCH 27/50] Rebase fixes --- chalk-ir/src/lib.rs | 18 +++++++++++------- chalk-solve/src/clauses.rs | 28 ++++++++++++++++++---------- 2 files changed, 29 insertions(+), 17 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 917aedfa82a..3b3bf9cbe1b 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -1512,13 +1512,17 @@ impl UCanonical { binders .iter() .enumerate() - .map(|(index, pk)| match pk { - ParameterKind::Ty(_) => { - ParameterKind::Ty(TyData::BoundVar(index).intern(interner)).intern(interner) - } - ParameterKind::Lifetime(_) => { - ParameterKind::Lifetime(LifetimeData::BoundVar(index).intern(interner)) - .intern(interner) + .map(|(index, pk)| { + let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, index); + match pk { + ParameterKind::Ty(_) => { + ParameterKind::Ty(TyData::BoundVar(bound_var).intern(interner)) + .intern(interner) + } + ParameterKind::Lifetime(_) => ParameterKind::Lifetime( + LifetimeData::BoundVar(bound_var).intern(interner), + ) + .intern(interner), } }) .collect::>(), diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 943612e89e9..8c5ca5a24b2 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -427,13 +427,13 @@ mod generalize { use chalk_ir::{ fold::{Fold, Folder}, interner::Interner, - Binders, Lifetime, LifetimeData, ParameterKind, Ty, TyData, + Binders, BoundVar, DebruijnIndex, Lifetime, LifetimeData, ParameterKind, Ty, TyData, }; use std::collections::HashMap; pub struct Generalize<'i, I: Interner> { binders: Vec>, - mapping: HashMap, + mapping: HashMap, interner: &'i I, } @@ -444,7 +444,9 @@ mod generalize { mapping: HashMap::new(), interner, }; - let value = value.fold_with(&mut generalize, 0).unwrap(); + let value = value + .fold_with(&mut generalize, DebruijnIndex::INNERMOST) + .unwrap(); Binders { binders: generalize.binders, value, @@ -457,28 +459,34 @@ mod generalize { self } - fn fold_free_var_ty(&mut self, depth: usize, binders: usize) -> Fallible> { + fn fold_free_var_ty( + &mut self, + bound_var: BoundVar, + outer_binder: DebruijnIndex, + ) -> Fallible> { let binder_vec = &mut self.binders; - let new_index = self.mapping.entry(depth).or_insert_with(|| { + let new_index = self.mapping.entry(bound_var).or_insert_with(|| { let i = binder_vec.len(); binder_vec.push(ParameterKind::Ty(())); i }); - Ok(TyData::BoundVar(*new_index + binders).intern(self.interner())) + let new_var = BoundVar::new(outer_binder, *new_index); + Ok(TyData::BoundVar(new_var).intern(self.interner())) } fn fold_free_var_lifetime( &mut self, - depth: usize, - binders: usize, + bound_var: BoundVar, + outer_binder: DebruijnIndex, ) -> Fallible> { let binder_vec = &mut self.binders; - let new_index = self.mapping.entry(depth).or_insert_with(|| { + let new_index = self.mapping.entry(bound_var).or_insert_with(|| { let i = binder_vec.len(); binder_vec.push(ParameterKind::Ty(())); i }); - Ok(LifetimeData::BoundVar(*new_index + binders).intern(self.interner())) + let new_var = BoundVar::new(outer_binder, *new_index); + Ok(LifetimeData::BoundVar(new_var).intern(self.interner())) } fn interner(&self) -> &'i I { From b1453e5bc70aeec41a44a55c824257866faefe91 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Mon, 30 Mar 2020 21:22:59 +0200 Subject: [PATCH 28/50] Undo floundering for AliasEq, it's not the right approach --- chalk-solve/src/recursive/mod.rs | 7 ------- 1 file changed, 7 deletions(-) diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index ef1062eb42d..6c9d9cdff33 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -556,13 +556,6 @@ impl<'me, I: Interner> Solver<'me, I> { } } - DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => { - let self_ty = alias_eq.alias.self_type_parameter(interner); - if let Some(_) = self_ty.bound(interner) { - return Err(Floundered); - } - } - DomainGoal::WellFormed(WellFormed::Ty(ty)) | DomainGoal::IsUpstream(ty) | DomainGoal::DownstreamType(ty) From 3a074e44482cceabcc743f62832a06ecffb52d7d Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 31 Mar 2020 20:22:08 +0200 Subject: [PATCH 29/50] Move floundering logic to program_clauses --- chalk-solve/src/clauses.rs | 65 ++++++++++++++++++++++++-------- chalk-solve/src/recursive/mod.rs | 30 +-------------- chalk-solve/src/solve/slg.rs | 35 ++--------------- 3 files changed, 54 insertions(+), 76 deletions(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 8c5ca5a24b2..7e2e2b35047 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -102,6 +102,8 @@ pub fn push_auto_trait_impls( }); } +// TODO add Floundered error instead of using Option + /// Given some goal `goal` that must be proven, along with /// its `environment`, figures out the program clauses that apply /// to this goal from the Rust program. So for example if the goal @@ -111,7 +113,7 @@ pub(crate) fn program_clauses_for_goal<'db, I: Interner>( db: &'db dyn RustIrDatabase, environment: &Environment, goal: &DomainGoal, -) -> Vec> { +) -> Option>> { debug_heading!( "program_clauses_for_goal(goal={:?}, environment={:?})", goal, @@ -121,13 +123,13 @@ pub(crate) fn program_clauses_for_goal<'db, I: Interner>( let mut vec = vec![]; vec.extend(db.custom_clauses()); - program_clauses_that_could_match(db, environment, goal, &mut vec); + program_clauses_that_could_match(db, environment, goal, &mut vec)?; program_clauses_for_env(db, environment, &mut vec); vec.retain(|c| c.could_match(interner, goal)); debug!("vec = {:#?}", vec); - vec + Some(vec) } /// Returns a set of program clauses that could possibly match @@ -139,7 +141,7 @@ fn program_clauses_that_could_match( environment: &Environment, goal: &DomainGoal, clauses: &mut Vec>, -) { +) -> Option<()> { let interner = db.interner(); let builder = &mut ClauseBuilder::new(db, clauses); @@ -147,9 +149,18 @@ fn program_clauses_that_could_match( DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => { let trait_id = trait_ref.trait_id; + let trait_datum = db.trait_datum(trait_id); + + if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() { + let self_ty = trait_ref.self_type_parameter(interner); + if self_ty.bound(interner).is_some() || self_ty.inference_var(interner).is_some() { + return None; + } + } + // This is needed for the coherence related impls, as well // as for the `Implemented(Foo) :- FromEnv(Foo)` rule. - db.trait_datum(trait_id).to_program_clauses(builder); + trait_datum.to_program_clauses(builder); for impl_id in db.impls_for_trait( trait_ref.trait_id, @@ -168,8 +179,8 @@ fn program_clauses_that_could_match( push_auto_trait_impls(builder, trait_id, struct_id); } } - TyData::InferenceVar(_) => { - panic!("auto-traits should flounder if nothing is known") + TyData::InferenceVar(_) | TyData::BoundVar(_) => { + return None; } _ => {} } @@ -262,12 +273,12 @@ fn program_clauses_that_could_match( } DomainGoal::WellFormed(WellFormed::Ty(ty)) | DomainGoal::IsUpstream(ty) - | DomainGoal::DownstreamType(ty) => match_ty(builder, environment, ty), + | DomainGoal::DownstreamType(ty) => match_ty(builder, environment, ty)?, DomainGoal::IsFullyVisible(ty) | DomainGoal::IsLocal(ty) => { - match_ty(builder, environment, ty) + match_ty(builder, environment, ty)? } DomainGoal::FromEnv(_) => (), // Computed in the environment - DomainGoal::Normalize(Normalize { alias, ty: _ }) => { + DomainGoal::Normalize(Normalize { alias, ty }) => { // Normalize goals derive from `AssociatedTyValue` datums, // which are found in impls. That is, if we are // normalizing (e.g.) `::Item>`, then @@ -282,6 +293,26 @@ fn program_clauses_that_could_match( let associated_ty_datum = db.associated_ty_data(alias.associated_ty_id); let trait_id = associated_ty_datum.trait_id; let trait_parameters = db.trait_parameters_from_projection(alias); + + if let TyData::Apply(ApplicationTy { + name: TypeName::AssociatedType(_), + .. + }) = ty.data(interner) + { + // TODO this is probably wrong + // Associated types will never *normalize* to an associated type placeholder. + // It's important that we return early here so that we don't flounder in this case. + return Some(()); + } + + let trait_datum = builder.db.trait_datum(trait_id); + if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() { + let self_ty = alias.self_type_parameter(interner); + if self_ty.bound(interner).is_some() || self_ty.inference_var(interner).is_some() { + return None; + } + } + push_program_clauses_for_associated_type_values_in_impls_of( builder, trait_id, @@ -293,6 +324,8 @@ fn program_clauses_that_could_match( .to_program_clauses(builder), DomainGoal::Compatible(()) => (), }; + + Some(()) } /// Generate program clauses from the associated-type values @@ -353,9 +386,9 @@ fn match_ty( builder: &mut ClauseBuilder<'_, I>, environment: &Environment, ty: &Ty, -) { +) -> Option<()> { let interner = builder.interner(); - match ty.data(interner) { + Some(match ty.data(interner) { TyData::Apply(application_ty) => match_type_name(builder, application_ty.name), TyData::Placeholder(_) => { builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone()))); @@ -370,12 +403,12 @@ fn match_ty( .substitution .iter(interner) .map(|p| p.assert_ty_ref(interner)) - .for_each(|ty| match_ty(builder, environment, &ty)) + .map(|ty| match_ty(builder, environment, &ty)) + .collect::>()?; } - TyData::BoundVar(_) => {} - TyData::InferenceVar(_) => panic!("should have floundered"), + TyData::BoundVar(_) | TyData::InferenceVar(_) => return None, TyData::Dyn(_) => {} - } + }) } fn match_type_name(builder: &mut ClauseBuilder<'_, I>, name: TypeName) { diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 6c9d9cdff33..dcde3e9e891 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -541,35 +541,7 @@ impl<'me, I: Interner> Solver<'me, I> { environment: &Environment, goal: &DomainGoal, ) -> Result>, Floundered> { - // TODO this is currently duplicated with the SLG solver, extract it somewhere? - // Look for floundering goals: - let interner = self.program.interner(); - match goal { - // Check for a goal like `?T: Foo` where `Foo` is not enumerable. - DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => { - let trait_datum = self.program.trait_datum(trait_ref.trait_id); - if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() { - let self_ty = trait_ref.self_type_parameter(interner); - if let Some(_) = self_ty.bound(interner) { - return Err(Floundered); - } - } - } - - DomainGoal::WellFormed(WellFormed::Ty(ty)) - | DomainGoal::IsUpstream(ty) - | DomainGoal::DownstreamType(ty) - | DomainGoal::IsFullyVisible(ty) - | DomainGoal::IsLocal(ty) => match ty.data(interner) { - TyData::BoundVar(_) => return Err(Floundered), - _ => {} - }, - - _ => {} - } - - // TODO this also includes clauses from env - Ok(program_clauses_for_goal(self.program, environment, goal)) + program_clauses_for_goal(self.program, environment, goal).ok_or(Floundered) } } diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs index 35e4aebb747..c918600e39a 100644 --- a/chalk-solve/src/solve/slg.rs +++ b/chalk-solve/src/solve/slg.rs @@ -175,39 +175,12 @@ impl<'me, I: Interner> context::ContextOps> for SlgContextOps<'me, &self, environment: &Environment, goal: &DomainGoal, - infer: &mut TruncatingInferenceTable, + _infer: &mut TruncatingInferenceTable, ) -> Result>, Floundered> { - // Look for floundering goals: - let interner = self.interner(); - match goal { - // Check for a goal like `?T: Foo` where `Foo` is not enumerable. - DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => { - let trait_datum = self.program.trait_datum(trait_ref.trait_id); - if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() { - let self_ty = trait_ref.self_type_parameter(interner); - if let Some(v) = self_ty.inference_var(interner) { - if !infer.infer.var_is_bound(v) { - return Err(Floundered); - } - } - } - } - - DomainGoal::WellFormed(WellFormed::Ty(ty)) - | DomainGoal::IsUpstream(ty) - | DomainGoal::DownstreamType(ty) - | DomainGoal::IsFullyVisible(ty) - | DomainGoal::IsLocal(ty) => match ty.data(interner) { - TyData::InferenceVar(_) => return Err(Floundered), - _ => {} - }, - - _ => {} - } - - let mut clauses: Vec<_> = program_clauses_for_goal(self.program, environment, goal); + let interner = self.program.interner(); + let mut clauses: Vec<_> = + program_clauses_for_goal(self.program, environment, goal).ok_or(Floundered)?; - // TODO this is redundant, I think clauses.extend( environment .clauses From ea15431e599f0510cc3ad29908b84af9507d441a Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 5 Apr 2020 12:03:58 +0200 Subject: [PATCH 30/50] Run tests with both solvers by default --- chalk-solve/src/solve.rs | 11 ++++++++--- tests/test/cycle.rs | 8 +++++++- tests/test/mod.rs | 27 ++++++++++++++++++++++----- tests/test/projection.rs | 2 +- tests/test/unify.rs | 8 +++++++- 5 files changed, 45 insertions(+), 11 deletions(-) diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index ad2652f878f..fcd870325ba 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -196,7 +196,7 @@ pub enum SolverChoice { } impl SolverChoice { - /// Returns the default SLG parameters. + /// Returns specific SLG parameters. pub fn slg(max_size: usize, expected_answers: Option) -> Self { SolverChoice::SLG { max_size, @@ -204,6 +204,11 @@ impl SolverChoice { } } + /// Returns the default SLG parameters. + pub fn slg_default() -> Self { + SolverChoice::slg(10, None) + } + /// Returns the default recursive solver setup. pub fn recursive() -> Self { SolverChoice::Recursive { @@ -234,8 +239,8 @@ impl SolverChoice { impl Default for SolverChoice { fn default() -> Self { - SolverChoice::recursive() - // SolverChoice::slg(10, None) + // SolverChoice::recursive() + SolverChoice::slg(10, None) } } diff --git a/tests/test/cycle.rs b/tests/test/cycle.rs index 4a8fa06cfc4..3e2a008cd9d 100644 --- a/tests/test/cycle.rs +++ b/tests/test/cycle.rs @@ -163,9 +163,15 @@ fn overflow() { // Will try to prove S>: Q then S>>: Q etc ad infinitum goal { S: Q - } yields { + } yields[SolverChoice::slg(10, None)] { "Ambiguous; no inference guidance" } + + goal { + S: Q + } yields[SolverChoice::recursive()] { + "No possible solution" + } } } diff --git a/tests/test/mod.rs b/tests/test/mod.rs index dc44a12fa86..2210dad8792 100644 --- a/tests/test/mod.rs +++ b/tests/test/mod.rs @@ -71,13 +71,15 @@ macro_rules! test { test!(@program[$program] @parsed_goals[ $($parsed_goals)* - (stringify!($goal), SolverChoice::default(), TestGoal::Aggregated($expected)) + (stringify!($goal), SolverChoice::slg_default(), TestGoal::Aggregated($expected)) + (stringify!($goal), SolverChoice::recursive(), TestGoal::Aggregated($expected)) ] @unparsed_goals[$($unparsed_goals)*]) }; - // goal { G } yields_all { "Y1", "Y2", ... , "YN" } -- test both solvers gets exactly N same answers in - // the same order + // goal { G } yields_all { "Y1", "Y2", ... , "YN" } -- test that the SLG + // solver gets exactly N answers in this order (the recursive solver can't + // return multiple answers) (@program[$program:tt] @parsed_goals[$($parsed_goals:tt)*] @unparsed_goals[ goal $goal:tt yields_all { $($expected:expr),* } $($unparsed_goals:tt)* @@ -85,12 +87,13 @@ macro_rules! test { test!(@program[$program] @parsed_goals[ $($parsed_goals)* - (stringify!($goal), SolverChoice::default(), TestGoal::All(vec![$($expected),*])) + (stringify!($goal), SolverChoice::slg_default(), TestGoal::All(vec![$($expected),*])) ] @unparsed_goals[$($unparsed_goals)*]) }; - // goal { G } yields_first { "Y1", "Y2", ... , "YN" } -- test both solvers gets at least N same first answers + // goal { G } yields_first { "Y1", "Y2", ... , "YN" } -- test that the SLG + // solver gets at least N same first answers (@program[$program:tt] @parsed_goals[$($parsed_goals:tt)*] @unparsed_goals[ goal $goal:tt yields_first { $($expected:expr),* } $($unparsed_goals:tt)* @@ -122,6 +125,20 @@ macro_rules! test { @unparsed_goals[goal $($unparsed_goals)*]) }; + // same as above, but there are multiple yields clauses => duplicate the goal + (@program[$program:tt] @parsed_goals[$($parsed_goals:tt)*] @unparsed_goals[ + goal $goal:tt + yields[$C:expr] { $expected:expr } + yields $($unparsed_tail:tt)* + ]) => { + test!(@program[$program] + @parsed_goals[ + $($parsed_goals)* + (stringify!($goal), $C, TestGoal::Aggregated($expected)) + ] + @unparsed_goals[goal $goal yields $($unparsed_tail)*]) + }; + // same as above, but for the final goal in the list. (@program[$program:tt] @parsed_goals[$($parsed_goals:tt)*] @unparsed_goals[ goal $goal:tt yields[$C:expr] { $expected:expr } diff --git a/tests/test/projection.rs b/tests/test/projection.rs index 0ba69b8e200..61ee421c0ec 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -142,7 +142,7 @@ fn projection_equality() { exists { S: Trait2 } - } yields { + } yields[SolverChoice::recursive()] { "Unique; substitution [?0 := u32]" } } diff --git a/tests/test/unify.rs b/tests/test/unify.rs index 2988fd9ef6f..31cbb6f47b9 100644 --- a/tests/test/unify.rs +++ b/tests/test/unify.rs @@ -108,11 +108,17 @@ fn unify_quantified_lifetimes() { } } } - } yields { + } yields[SolverChoice::slg(10, None)] { "Unique; for { \ substitution [?0 := '^0.0, ?1 := '!1_0], \ lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \ }" + } yields[SolverChoice::recursive()] { + // only difference is in the value of ?1, which is equivalent + "Unique; for { \ + substitution [?0 := '^0.0, ?1 := '^0.0], \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \ + }" } } } From 62b0da6f173805d3cae1a9895cd7d75d504974b4 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 5 Apr 2020 12:20:06 +0200 Subject: [PATCH 31/50] Fix futures_ambiguity test --- chalk-solve/src/clauses.rs | 21 +-------------------- chalk-solve/src/recursive/mod.rs | 6 +++++- 2 files changed, 6 insertions(+), 21 deletions(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 7e2e2b35047..f284907f4eb 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -278,7 +278,7 @@ fn program_clauses_that_could_match( match_ty(builder, environment, ty)? } DomainGoal::FromEnv(_) => (), // Computed in the environment - DomainGoal::Normalize(Normalize { alias, ty }) => { + DomainGoal::Normalize(Normalize { alias, ty: _ }) => { // Normalize goals derive from `AssociatedTyValue` datums, // which are found in impls. That is, if we are // normalizing (e.g.) `::Item>`, then @@ -294,25 +294,6 @@ fn program_clauses_that_could_match( let trait_id = associated_ty_datum.trait_id; let trait_parameters = db.trait_parameters_from_projection(alias); - if let TyData::Apply(ApplicationTy { - name: TypeName::AssociatedType(_), - .. - }) = ty.data(interner) - { - // TODO this is probably wrong - // Associated types will never *normalize* to an associated type placeholder. - // It's important that we return early here so that we don't flounder in this case. - return Some(()); - } - - let trait_datum = builder.db.trait_datum(trait_id); - if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() { - let self_ty = alias.self_type_parameter(interner); - if self_ty.bound(interner).is_some() || self_ty.inference_var(interner).is_some() { - return None; - } - } - push_program_clauses_for_associated_type_values_in_impls_of( builder, trait_id, diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index dcde3e9e891..7aff4df8ddc 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -333,10 +333,14 @@ impl<'me, I: Interner> Solver<'me, I> { self.context.search_graph[dfn].solution_priority, current_prio, ) == (ClausePriority::High, ClausePriority::Low) + && self.context.search_graph[dfn].solution.is_ok() { // TODO check solution inputs? // Not replacing the current answer, so we're at a fixed point? - debug!("solve_new_subgoal: new answer has lower priority"); + debug!( + "solve_new_subgoal: new answer has lower priority (old answer: {:?})", + self.context.search_graph[dfn].solution + ); return *minimums; } From 9374586d8177e96a5f29f3163f6547b00312f34b Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sun, 5 Apr 2020 12:30:10 +0200 Subject: [PATCH 32/50] Make program_clauses_for_env add the actual env clauses as well The `program_clauses_for_env` function only added elaborated clauses, not the actual clauses from the environment. Instead, both solvers added the clauses afterwards. It seems easier to just add the direct clauses as well. --- chalk-solve/src/clauses.rs | 2 ++ chalk-solve/src/recursive/mod.rs | 27 +-------------------------- chalk-solve/src/solve.rs | 26 -------------------------- chalk-solve/src/solve/slg.rs | 13 ++----------- 4 files changed, 5 insertions(+), 63 deletions(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index f284907f4eb..d825a220726 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -415,6 +415,8 @@ fn program_clauses_for_env<'db, I: Interner>( environment: &Environment, clauses: &mut Vec>, ) { + clauses.extend(environment.clauses.iter().cloned()); + let mut last_round = FxHashSet::default(); elaborate_env_clauses( db, diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 7aff4df8ddc..e8c7d72f643 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -11,7 +11,6 @@ use chalk_engine::{ context::Floundered, fallible::{Fallible, NoSolution}, }; -use chalk_ir::could_match::CouldMatch; use clauses::program_clauses_for_goal; use rustc_hash::FxHashMap; @@ -253,19 +252,6 @@ impl<'me, I: Interner> Solver<'me, I> { // clauses. We try each approach in turn: let InEnvironment { environment, goal } = &canonical_goal.canonical.value; - let (env_solution, env_prio) = { - debug_heading!("env_clauses"); - - // TODO use code from clauses module - let env_clauses: Vec<_> = environment - .clauses - .iter() - .filter(|&clause| clause.could_match(self.program.interner(), goal)) - .cloned() - .collect(); - self.solve_from_clauses(&canonical_goal, env_clauses, minimums) - }; - debug!("env_solution={:?}", env_solution); let (prog_solution, prog_prio) = { debug_heading!("prog_clauses"); @@ -282,18 +268,7 @@ impl<'me, I: Interner> Solver<'me, I> { }; debug!("prog_solution={:?}", prog_solution); - // Now that we have all the outcomes, we attempt to combine - // them. Here, we apply a heuristic (also found in rustc): if we - // have possible solutions via both the environment *and* the - // program, we favor the environment; this only impacts type - // inference. The idea is that the assumptions you've explicitly - // made in a given context are more likely to be relevant than - // general `impl`s. - // TODO can we combine this logic with the priorization logic? - ( - env_solution.merge_with(prog_solution, |env, prog| env.favor_over(prog)), - prog_prio & env_prio, // FIXME - ) + (prog_solution, prog_prio) } _ => { diff --git a/chalk-solve/src/solve.rs b/chalk-solve/src/solve.rs index fcd870325ba..a8e72282f95 100644 --- a/chalk-solve/src/solve.rs +++ b/chalk-solve/src/solve.rs @@ -92,32 +92,6 @@ impl Solution { Solution::Ambig(guidance) } - /// There are multiple candidate solutions, which may or may not agree on - /// the values for existential variables; attempt to combine them, while - /// favoring `self` for the purposes of giving suggestions to type - /// inference. This is used in particular to favor the `where` clause - /// environment over `impl`s in guiding inference in ambiguous situations. - /// - /// It should always be the case that `x.favor_over(y)` is at least as - /// informative as `x.combine(y)`, in terms of guidance to type inference. - pub(crate) fn favor_over(self, other: Solution) -> Solution { - use self::Guidance::*; - - if self == other { - return self; - } - - debug!("favor_over {} with {}", self, other); - - // Otherwise, always downgrade to Ambig: - - let guidance = match (self.into_guidance(), other.into_guidance()) { - (Definite(subst), _) | (Suggested(subst), _) => Suggested(subst), - _ => Unknown, - }; - Solution::Ambig(guidance) - } - /// View this solution purely in terms of type inference guidance pub(crate) fn into_guidance(self) -> Guidance { match self { diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs index c918600e39a..93e8759ffa9 100644 --- a/chalk-solve/src/solve/slg.rs +++ b/chalk-solve/src/solve/slg.rs @@ -15,7 +15,7 @@ use chalk_engine::{CompleteAnswer, ExClause, Literal}; use chalk_ir::cast::Cast; use chalk_ir::cast::Caster; use chalk_ir::could_match::CouldMatch; -use chalk_ir::interner::Interner; +use chalk_ir::interner::{HasInterner, Interner}; use chalk_ir::*; use std::fmt::Debug; @@ -177,18 +177,9 @@ impl<'me, I: Interner> context::ContextOps> for SlgContextOps<'me, goal: &DomainGoal, _infer: &mut TruncatingInferenceTable, ) -> Result>, Floundered> { - let interner = self.program.interner(); - let mut clauses: Vec<_> = + let clauses: Vec<_> = program_clauses_for_goal(self.program, environment, goal).ok_or(Floundered)?; - clauses.extend( - environment - .clauses - .iter(interner) - .filter(|&env_clause| env_clause.could_match(interner, goal)) - .cloned(), - ); - Ok(clauses) } From 27f9ef711ec2fcebb88ba8a7a2c061bf0308e1b2 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Fri, 10 Apr 2020 15:25:05 +0200 Subject: [PATCH 33/50] Rebase fixes --- chalk-ir/src/lib.rs | 2 +- chalk-ir/src/visit/boring_impls.rs | 3 ++- chalk-solve/src/clauses.rs | 2 +- chalk-solve/src/recursive/fulfill.rs | 5 +++-- chalk-solve/src/recursive/mod.rs | 14 +++++++------- chalk-solve/src/solve/slg/resolvent.rs | 4 ++-- 6 files changed, 16 insertions(+), 14 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 3b3bf9cbe1b..b951452abfd 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -547,7 +547,7 @@ impl DebruijnIndex { /// known. It is referenced within the type using `^1`, indicating /// a bound type with debruijn index 1 (i.e., skipping through one /// level of binder). -#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit)] +#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)] pub struct DynTy { pub bounds: Binders>, } diff --git a/chalk-ir/src/visit/boring_impls.rs b/chalk-ir/src/visit/boring_impls.rs index 45a513752bd..a78bd6c3785 100644 --- a/chalk-ir/src/visit/boring_impls.rs +++ b/chalk-ir/src/visit/boring_impls.rs @@ -5,7 +5,7 @@ //! The more interesting impls of `Visit` remain in the `visit` module. use crate::{ - AssocTypeId, DebruijnIndex, Goals, ImplId, Interner, Parameter, ParameterKind, + AssocTypeId, ClausePriority, DebruijnIndex, Goals, ImplId, Interner, Parameter, ParameterKind, PlaceholderIndex, ProgramClause, ProgramClauseData, ProgramClauses, QuantifiedWhereClauses, QuantifierKind, StructId, Substitution, SuperVisit, TraitId, UniverseIndex, Visit, VisitResult, Visitor, @@ -205,6 +205,7 @@ const_visit!(QuantifierKind); const_visit!(DebruijnIndex); const_visit!(chalk_engine::TableIndex); const_visit!(chalk_engine::TimeStamp); +const_visit!(ClausePriority); const_visit!(()); #[macro_export] diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index d825a220726..fc23f8d5524 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -415,7 +415,7 @@ fn program_clauses_for_env<'db, I: Interner>( environment: &Environment, clauses: &mut Vec>, ) { - clauses.extend(environment.clauses.iter().cloned()); + clauses.extend(environment.clauses.iter(db.interner()).cloned()); let mut last_round = FxHashSet::default(); elaborate_env_clauses( diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index 65c332a0a3d..7bc1da3151c 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -183,7 +183,8 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { self.push_goal(environment, subgoal)?; } GoalData::Implies(wc, subgoal) => { - let new_environment = &environment.add_clauses(wc.iter().cloned()); + let new_environment = + &environment.add_clauses(interner, wc.iter(interner).cloned()); self.push_goal(new_environment, subgoal.clone())?; } GoalData::All(goals) => { @@ -293,7 +294,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { // We use the empty environment for unification here because we're // really just doing a substitution on unconstrained variables, which is // guaranteed to succeed without generating any new constraints. - let empty_env = &Environment::new(); + let empty_env = &Environment::new(self.solver.program.interner()); for (i, free_var) in free_vars.into_iter().enumerate() { let subst_value = subst.at(self.interner(), i); diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index e8c7d72f643..43ed8d6f485 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -395,13 +395,13 @@ impl<'me, I: Interner> Solver<'me, I> { for program_clause in clauses { debug_heading!("clause={:?}", program_clause); - match program_clause { - ProgramClause::Implies(implication) => { + match program_clause.data(self.program.interner()) { + ProgramClauseData::Implies(implication) => { let res = self.solve_via_implication( canonical_goal, - Binders { + &Binders { binders: vec![], - value: implication, + value: implication.clone(), }, minimums, ); @@ -436,7 +436,7 @@ impl<'me, I: Interner> Solver<'me, I> { debug!("error"); } } - ProgramClause::ForAll(implication) => { + ProgramClauseData::ForAll(implication) => { let res = self.solve_via_implication(canonical_goal, implication, minimums); if let (Ok(solution), priority) = res { debug!("ok: solution={:?} prio={:?}", solution, priority); @@ -480,7 +480,7 @@ impl<'me, I: Interner> Solver<'me, I> { fn solve_via_implication( &mut self, canonical_goal: &UCanonical>>, - clause: Binders>, + clause: &Binders>, minimums: &mut Minimums, ) -> (Fallible>, ClausePriority) { info_heading!( @@ -496,7 +496,7 @@ impl<'me, I: Interner> Solver<'me, I> { consequence, conditions, priority: _, - } = fulfill.instantiate_binders_existentially(&clause); + } = fulfill.instantiate_binders_existentially(clause); debug!("the subst is {:?}", subst); diff --git a/chalk-solve/src/solve/slg/resolvent.rs b/chalk-solve/src/solve/slg/resolvent.rs index 6c0478e406f..89d39388c96 100644 --- a/chalk-solve/src/solve/slg/resolvent.rs +++ b/chalk-solve/src/solve/slg/resolvent.rs @@ -85,8 +85,8 @@ impl context::ResolventOps> for TruncatingInferenceTa conditions, priority: _, } = match clause.data(interner) { - ProgramClause::Implies(implication) => implication.clone(), - ProgramClause::ForAll(implication) => self + ProgramClauseData::Implies(implication) => implication.clone(), + ProgramClauseData::ForAll(implication) => self .infer .instantiate_binders_existentially(interner, implication), }; From 60b389261eabc81e42fb799bc0b4f67ea3bf02ec Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Fri, 10 Apr 2020 17:10:26 +0200 Subject: [PATCH 34/50] Use Floundered error in program_clauses --- chalk-solve/src/clauses.rs | 23 +++++++++++------------ chalk-solve/src/recursive/mod.rs | 2 +- chalk-solve/src/solve/slg.rs | 3 +-- 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index fc23f8d5524..04373404f7e 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -3,6 +3,7 @@ use self::env_elaborator::elaborate_env_clauses; use self::program_clauses::ToProgramClauses; use crate::split::Split; use crate::RustIrDatabase; +use chalk_engine::context::Floundered; use chalk_ir::cast::Cast; use chalk_ir::could_match::CouldMatch; use chalk_ir::interner::Interner; @@ -102,8 +103,6 @@ pub fn push_auto_trait_impls( }); } -// TODO add Floundered error instead of using Option - /// Given some goal `goal` that must be proven, along with /// its `environment`, figures out the program clauses that apply /// to this goal from the Rust program. So for example if the goal @@ -113,7 +112,7 @@ pub(crate) fn program_clauses_for_goal<'db, I: Interner>( db: &'db dyn RustIrDatabase, environment: &Environment, goal: &DomainGoal, -) -> Option>> { +) -> Result>, Floundered> { debug_heading!( "program_clauses_for_goal(goal={:?}, environment={:?})", goal, @@ -129,7 +128,7 @@ pub(crate) fn program_clauses_for_goal<'db, I: Interner>( debug!("vec = {:#?}", vec); - Some(vec) + Ok(vec) } /// Returns a set of program clauses that could possibly match @@ -141,7 +140,7 @@ fn program_clauses_that_could_match( environment: &Environment, goal: &DomainGoal, clauses: &mut Vec>, -) -> Option<()> { +) -> Result<(), Floundered> { let interner = db.interner(); let builder = &mut ClauseBuilder::new(db, clauses); @@ -154,7 +153,7 @@ fn program_clauses_that_could_match( if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() { let self_ty = trait_ref.self_type_parameter(interner); if self_ty.bound(interner).is_some() || self_ty.inference_var(interner).is_some() { - return None; + return Err(Floundered); } } @@ -180,7 +179,7 @@ fn program_clauses_that_could_match( } } TyData::InferenceVar(_) | TyData::BoundVar(_) => { - return None; + return Err(Floundered); } _ => {} } @@ -306,7 +305,7 @@ fn program_clauses_that_could_match( DomainGoal::Compatible(()) => (), }; - Some(()) + Ok(()) } /// Generate program clauses from the associated-type values @@ -367,9 +366,9 @@ fn match_ty( builder: &mut ClauseBuilder<'_, I>, environment: &Environment, ty: &Ty, -) -> Option<()> { +) -> Result<(), Floundered> { let interner = builder.interner(); - Some(match ty.data(interner) { + Ok(match ty.data(interner) { TyData::Apply(application_ty) => match_type_name(builder, application_ty.name), TyData::Placeholder(_) => { builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone()))); @@ -385,9 +384,9 @@ fn match_ty( .iter(interner) .map(|p| p.assert_ty_ref(interner)) .map(|ty| match_ty(builder, environment, &ty)) - .collect::>()?; + .collect::>()?; } - TyData::BoundVar(_) | TyData::InferenceVar(_) => return None, + TyData::BoundVar(_) | TyData::InferenceVar(_) => return Err(Floundered), TyData::Dyn(_) => {} }) } diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 43ed8d6f485..1fe2f57bf26 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -520,7 +520,7 @@ impl<'me, I: Interner> Solver<'me, I> { environment: &Environment, goal: &DomainGoal, ) -> Result>, Floundered> { - program_clauses_for_goal(self.program, environment, goal).ok_or(Floundered) + program_clauses_for_goal(self.program, environment, goal) } } diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs index 93e8759ffa9..33d90338bd9 100644 --- a/chalk-solve/src/solve/slg.rs +++ b/chalk-solve/src/solve/slg.rs @@ -177,8 +177,7 @@ impl<'me, I: Interner> context::ContextOps> for SlgContextOps<'me, goal: &DomainGoal, _infer: &mut TruncatingInferenceTable, ) -> Result>, Floundered> { - let clauses: Vec<_> = - program_clauses_for_goal(self.program, environment, goal).ok_or(Floundered)?; + let clauses: Vec<_> = program_clauses_for_goal(self.program, environment, goal)?; Ok(clauses) } From 835fa6855ea621647dc806edf5da2cb87d6519cf Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Fri, 10 Apr 2020 17:19:09 +0200 Subject: [PATCH 35/50] Make the prioritization code slightly nicer --- chalk-solve/src/recursive/mod.rs | 118 ++++++++++++++----------------- 1 file changed, 52 insertions(+), 66 deletions(-) diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 1fe2f57bf26..97564e4c685 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -364,34 +364,7 @@ impl<'me, I: Interner> Solver<'me, I> { where C: IntoIterator>, { - // TODO we don't actually need to keep track of the inputs let mut cur_solution = None; - fn combine_with_priorities( - a: Solution, - prio_a: ClausePriority, - inputs_a: Vec>, - b: Solution, - prio_b: ClausePriority, - inputs_b: Vec>, - ) -> (Solution, ClausePriority, Vec>) { - match (prio_a, prio_b) { - (ClausePriority::High, ClausePriority::Low) if inputs_a == inputs_b => { - debug!( - "preferring solution: {:?} over {:?} because of higher prio", - a, b - ); - (a, ClausePriority::High, inputs_a) - } - (ClausePriority::Low, ClausePriority::High) if inputs_a == inputs_b => { - debug!( - "preferring solution: {:?} over {:?} because of higher prio", - b, a - ); - (b, ClausePriority::High, inputs_b) - } - _ => (a.combine(b), prio_a, inputs_a), - } - } for program_clause in clauses { debug_heading!("clause={:?}", program_clause); @@ -407,29 +380,15 @@ impl<'me, I: Interner> Solver<'me, I> { ); if let (Ok(solution), priority) = res { debug!("ok: solution={:?} prio={:?}", solution, priority); - let inputs = if let Some(subst) = solution.constrained_subst() { - let subst_goal = subst.value.subst.apply( - &canonical_goal.canonical.value.goal, - self.program.interner(), - ); - debug!("subst_goal = {:?}", subst_goal); - subst_goal.inputs(self.program.interner()) - } else { - canonical_goal - .canonical - .value - .goal - .inputs(self.program.interner()) - }; cur_solution = Some(match cur_solution { - None => (solution, priority, inputs), - Some((cur, cur_priority, cur_inputs)) => combine_with_priorities( + None => (solution, priority), + Some((cur, cur_priority)) => combine_with_priorities( + self.program.interner(), + canonical_goal, cur, cur_priority, - cur_inputs, solution, priority, - inputs, ), }); } else { @@ -440,29 +399,15 @@ impl<'me, I: Interner> Solver<'me, I> { let res = self.solve_via_implication(canonical_goal, implication, minimums); if let (Ok(solution), priority) = res { debug!("ok: solution={:?} prio={:?}", solution, priority); - let inputs = if let Some(subst) = solution.constrained_subst() { - let subst_goal = subst.value.subst.apply( - &canonical_goal.canonical.value.goal, - self.program.interner(), - ); - debug!("subst_goal = {:?}", subst_goal); - subst_goal.inputs(self.program.interner()) - } else { - canonical_goal - .canonical - .value - .goal - .inputs(self.program.interner()) - }; cur_solution = Some(match cur_solution { - None => (solution, priority, inputs), - Some((cur, cur_priority, cur_inputs)) => combine_with_priorities( + None => (solution, priority), + Some((cur, cur_priority)) => combine_with_priorities( + self.program.interner(), + canonical_goal, cur, cur_priority, - cur_inputs, solution, priority, - inputs, ), }); } else { @@ -471,9 +416,7 @@ impl<'me, I: Interner> Solver<'me, I> { } } } - cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p, _)| { - (Ok(s), p) - }) + cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p)| (Ok(s), p)) } /// Modus ponens! That is: try to apply an implication by proving its premises. @@ -524,6 +467,49 @@ impl<'me, I: Interner> Solver<'me, I> { } } +fn calculate_inputs( + interner: &I, + canonical_goal: &UCanonical>>, + solution: &Solution, +) -> Vec> { + if let Some(subst) = solution.constrained_subst() { + let subst_goal = subst + .value + .subst + .apply(&canonical_goal.canonical.value.goal, interner); + subst_goal.inputs(interner) + } else { + canonical_goal.canonical.value.goal.inputs(interner) + } +} + +fn combine_with_priorities( + interner: &I, + canonical_goal: &UCanonical>>, + a: Solution, + prio_a: ClausePriority, + b: Solution, + prio_b: ClausePriority, +) -> (Solution, ClausePriority) { + match (prio_a, prio_b, a, b) { + (ClausePriority::High, ClausePriority::Low, higher, lower) + | (ClausePriority::Low, ClausePriority::High, lower, higher) => { + let inputs_higher = calculate_inputs(interner, canonical_goal, &higher); + let inputs_lower = calculate_inputs(interner, canonical_goal, &lower); + if inputs_higher == inputs_lower { + debug!( + "preferring solution: {:?} over {:?} because of higher prio", + higher, lower + ); + (higher, ClausePriority::High) + } else { + (higher.combine(lower), ClausePriority::High) + } + } + (_, _, a, b) => (a.combine(b), prio_a), + } +} + impl Minimums { fn new() -> Self { Minimums { From 9166f3efda67122062c376827472669ebba0e126 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Fri, 10 Apr 2020 17:24:10 +0200 Subject: [PATCH 36/50] Add another test --- tests/test/projection.rs | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/tests/test/projection.rs b/tests/test/projection.rs index 61ee421c0ec..a2a56a0a6d1 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -148,6 +148,31 @@ fn projection_equality() { } } +#[test] +fn projection_equality_from_env() { + test! { + program { + trait Trait1 { + type Type; + } + + struct u32 {} + } + + goal { + forall { + if (T: Trait1) { + exists { + ::Type = U + } + } + } + } yields[SolverChoice::recursive()] { + "Unique; substitution [?0 := u32]" + } + } +} + #[test] fn normalize_gat1() { test! { From 2d193f3aeeef77df09459d275c2e5a39252e4ed1 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Fri, 10 Apr 2020 17:26:46 +0200 Subject: [PATCH 37/50] Move generalizer to its own module --- chalk-solve/src/clauses.rs | 78 +------------------------- chalk-solve/src/clauses/generalize.rs | 80 +++++++++++++++++++++++++++ 2 files changed, 81 insertions(+), 77 deletions(-) create mode 100644 chalk-solve/src/clauses/generalize.rs diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 04373404f7e..19dfd0cfbec 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -13,6 +13,7 @@ use rustc_hash::FxHashSet; pub mod builder; mod builtin_traits; mod env_elaborator; +mod generalize; pub mod program_clauses; /// For auto-traits, we generate a default rule for every struct, @@ -436,80 +437,3 @@ fn program_clauses_for_env<'db, I: Interner>( clauses.extend(closure.drain()) } - -mod generalize { - use chalk_engine::fallible::Fallible; - use chalk_ir::{ - fold::{Fold, Folder}, - interner::Interner, - Binders, BoundVar, DebruijnIndex, Lifetime, LifetimeData, ParameterKind, Ty, TyData, - }; - use std::collections::HashMap; - - pub struct Generalize<'i, I: Interner> { - binders: Vec>, - mapping: HashMap, - interner: &'i I, - } - - impl Generalize<'_, I> { - pub fn apply>(interner: &I, value: &T) -> Binders { - let mut generalize = Generalize { - binders: Vec::new(), - mapping: HashMap::new(), - interner, - }; - let value = value - .fold_with(&mut generalize, DebruijnIndex::INNERMOST) - .unwrap(); - Binders { - binders: generalize.binders, - value, - } - } - } - - impl<'i, I: Interner> Folder<'i, I> for Generalize<'i, I> { - fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> { - self - } - - fn fold_free_var_ty( - &mut self, - bound_var: BoundVar, - outer_binder: DebruijnIndex, - ) -> Fallible> { - let binder_vec = &mut self.binders; - let new_index = self.mapping.entry(bound_var).or_insert_with(|| { - let i = binder_vec.len(); - binder_vec.push(ParameterKind::Ty(())); - i - }); - let new_var = BoundVar::new(outer_binder, *new_index); - Ok(TyData::BoundVar(new_var).intern(self.interner())) - } - - fn fold_free_var_lifetime( - &mut self, - bound_var: BoundVar, - outer_binder: DebruijnIndex, - ) -> Fallible> { - let binder_vec = &mut self.binders; - let new_index = self.mapping.entry(bound_var).or_insert_with(|| { - let i = binder_vec.len(); - binder_vec.push(ParameterKind::Ty(())); - i - }); - let new_var = BoundVar::new(outer_binder, *new_index); - Ok(LifetimeData::BoundVar(new_var).intern(self.interner())) - } - - fn interner(&self) -> &'i I { - self.interner - } - - fn target_interner(&self) -> &'i I { - self.interner - } - } -} diff --git a/chalk-solve/src/clauses/generalize.rs b/chalk-solve/src/clauses/generalize.rs new file mode 100644 index 00000000000..c1babc0b95e --- /dev/null +++ b/chalk-solve/src/clauses/generalize.rs @@ -0,0 +1,80 @@ +//! This gets rid of free variables in a type by replacing them by fresh bound +//! ones. We use this when building clauses that contain types passed to +//! `program_clauses`; these may contain variables, and just copying those +//! variables verbatim leads to problems. Instead, we return a slightly more +//! general program clause, with new variables in those places. + +use chalk_engine::fallible::Fallible; +use chalk_ir::{ + fold::{Fold, Folder}, + interner::Interner, + Binders, BoundVar, DebruijnIndex, Lifetime, LifetimeData, ParameterKind, Ty, TyData, +}; +use std::collections::HashMap; + +pub struct Generalize<'i, I: Interner> { + binders: Vec>, + mapping: HashMap, + interner: &'i I, +} + +impl Generalize<'_, I> { + pub fn apply>(interner: &I, value: &T) -> Binders { + let mut generalize = Generalize { + binders: Vec::new(), + mapping: HashMap::new(), + interner, + }; + let value = value + .fold_with(&mut generalize, DebruijnIndex::INNERMOST) + .unwrap(); + Binders { + binders: generalize.binders, + value, + } + } +} + +impl<'i, I: Interner> Folder<'i, I> for Generalize<'i, I> { + fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> { + self + } + + fn fold_free_var_ty( + &mut self, + bound_var: BoundVar, + outer_binder: DebruijnIndex, + ) -> Fallible> { + let binder_vec = &mut self.binders; + let new_index = self.mapping.entry(bound_var).or_insert_with(|| { + let i = binder_vec.len(); + binder_vec.push(ParameterKind::Ty(())); + i + }); + let new_var = BoundVar::new(outer_binder, *new_index); + Ok(TyData::BoundVar(new_var).intern(self.interner())) + } + + fn fold_free_var_lifetime( + &mut self, + bound_var: BoundVar, + outer_binder: DebruijnIndex, + ) -> Fallible> { + let binder_vec = &mut self.binders; + let new_index = self.mapping.entry(bound_var).or_insert_with(|| { + let i = binder_vec.len(); + binder_vec.push(ParameterKind::Ty(())); + i + }); + let new_var = BoundVar::new(outer_binder, *new_index); + Ok(LifetimeData::BoundVar(new_var).intern(self.interner())) + } + + fn interner(&self) -> &'i I { + self.interner + } + + fn target_interner(&self) -> &'i I { + self.interner + } +} From d69da2fe92fc79ddd9a99db9ebe745a224f13253 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sat, 11 Apr 2020 12:15:44 +0200 Subject: [PATCH 38/50] Add back Normalize floundering --- chalk-solve/src/clauses.rs | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 19dfd0cfbec..7eb6041ec3c 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -278,7 +278,7 @@ fn program_clauses_that_could_match( match_ty(builder, environment, ty)? } DomainGoal::FromEnv(_) => (), // Computed in the environment - DomainGoal::Normalize(Normalize { alias, ty: _ }) => { + DomainGoal::Normalize(Normalize { alias, ty }) => { // Normalize goals derive from `AssociatedTyValue` datums, // which are found in impls. That is, if we are // normalizing (e.g.) `::Item>`, then @@ -294,6 +294,35 @@ fn program_clauses_that_could_match( let trait_id = associated_ty_datum.trait_id; let trait_parameters = db.trait_parameters_from_projection(alias); + if (alias + .self_type_parameter(interner) + .bound(interner) + .is_some() + || alias + .self_type_parameter(interner) + .inference_var(interner) + .is_some()) + && (ty.bound(interner).is_some() || ty.inference_var(interner).is_some()) + { + return Err(Floundered); + } + + let trait_datum = db.trait_datum(trait_id); + + // FIXME + if (alias + .self_type_parameter(interner) + .bound(interner) + .is_some() + || alias + .self_type_parameter(interner) + .inference_var(interner) + .is_some()) + && trait_datum.is_non_enumerable_trait() + { + return Err(Floundered); + } + push_program_clauses_for_associated_type_values_in_impls_of( builder, trait_id, From 31d6f2a81e22e58841d8d171901bdf836e1f6100 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Sat, 11 Apr 2020 12:16:09 +0200 Subject: [PATCH 39/50] Increase hard-coded max size to 30 --- chalk-solve/src/recursive/fulfill.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index 7bc1da3151c..82276a8e996 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -126,12 +126,12 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let obligation = match obligation { Obligation::Prove(goal) => { let truncated = - truncate::truncate(self.solver.program.interner(), &mut self.infer, 10, &goal); + truncate::truncate(self.solver.program.interner(), &mut self.infer, 30, &goal); Obligation::Prove(truncated.value) } Obligation::Refute(goal) => { let truncated = - truncate::truncate(self.solver.program.interner(), &mut self.infer, 10, &goal); + truncate::truncate(self.solver.program.interner(), &mut self.infer, 30, &goal); Obligation::Refute(truncated.value) } }; From f6c162341559e5de93d3d20b001233a69357076d Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 14 Apr 2020 12:12:07 +0200 Subject: [PATCH 40/50] Add some more tests --- tests/test/projection.rs | 68 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 68 insertions(+) diff --git a/tests/test/projection.rs b/tests/test/projection.rs index a2a56a0a6d1..2be323d7594 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -173,6 +173,74 @@ fn projection_equality_from_env() { } } +#[test] +fn projection_equality_nested() { + test! { + program { + trait Iterator { + type Item; + } + + struct u32 {} + } + + goal { + forall { + if (I: Iterator) { + if (::Item: Iterator) { + exists { + <::Item as Iterator>::Item = U + } + } + } + } + } yields[SolverChoice::recursive()] { + "Unique; substitution [?0 := u32]" + } + } +} + +#[test] +fn iterator_flatten() { + test! { + program { + trait Iterator { + type Item; + } + #[non_enumerable] + trait IntoIterator { + type Item; + type IntoIter: Iterator::Item>; + } + struct Flatten {} + + impl Iterator for Flatten + where + I: Iterator, + ::Item: IntoIterator, + ::Item: IntoIterator::Item>, + U: Iterator + { + type Item = ::Item; + } + + struct u32 {} + } + + goal { + forall { + if (I: Iterator; U: IntoIterator) { + exists { + as Iterator>::Item = T + } + } + } + } yields[SolverChoice::recursive()] { + "Unique; substitution [?0 := u32]" + } + } +} + #[test] fn normalize_gat1() { test! { From 0abdef909bebb2f81ecd0ad929361ebea008a2e4 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 14 Apr 2020 12:13:13 +0200 Subject: [PATCH 41/50] Don't inherit clause priority in implications So if we had some implication A => B, if the solution for A had low priority, we also made B low priority. After some testing, I don't think this is right. --- chalk-solve/src/recursive/fulfill.rs | 29 +++++++++------------------- chalk-solve/src/recursive/mod.rs | 29 +++++++++++++--------------- 2 files changed, 22 insertions(+), 36 deletions(-) diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index 82276a8e996..7f2b3008c67 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -75,8 +75,6 @@ pub(crate) struct Fulfill<'s, 'db, I: Interner> { /// The remaining goals to prove or refute obligations: Vec>, - priority: ClausePriority, - /// Lifetime constraints that must be fulfilled for a solution to be fully /// validated. constraints: HashSet>>, @@ -91,7 +89,6 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { pub(crate) fn new + HasInterner + Clone>( solver: &'s mut Solver<'db, I>, ucanonical_goal: &UCanonical>, - priority: ClausePriority, ) -> (Self, Substitution, InEnvironment) { let (infer, subst, canonical_goal) = InferenceTable::from_canonical( solver.program.interner(), @@ -102,7 +99,6 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { solver, infer, obligations: vec![], - priority, constraints: HashSet::new(), cannot_prove: false, }; @@ -225,8 +221,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { quantified, universes, } = self.infer.u_canonicalize(interner, &quantified); - let (result, new_priority) = self.solver.solve_goal(quantified, minimums); - self.priority = self.priority & new_priority; + let result = self.solver.solve_goal(quantified, minimums); Ok(PositiveSolution { free_vars, universes, @@ -255,7 +250,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { .infer .u_canonicalize(self.solver.program.interner(), &canonicalized); let mut minimums = Minimums::new(); // FIXME -- minimums here seems wrong - if let (Ok(solution), _priority) = self.solver.solve_goal(quantified, &mut minimums) { + if let Ok(solution) = self.solver.solve_goal(quantified, &mut minimums) { if solution.is_unique() { Err(NoSolution) } else { @@ -384,14 +379,14 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { mut self, subst: Substitution, minimums: &mut Minimums, - ) -> (Fallible>, ClausePriority) { + ) -> Fallible> { let outcome = match self.fulfill(minimums) { Ok(o) => o, - Err(e) => return (Err(e), self.priority), + Err(e) => return Err(e), }; if self.cannot_prove { - return (Ok(Solution::Ambig(Guidance::Unknown)), self.priority); + return Ok(Solution::Ambig(Guidance::Unknown)); } if outcome.is_complete() { @@ -403,7 +398,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { self.solver.program.interner(), &ConstrainedSubst { subst, constraints }, ); - return (Ok(Solution::Unique(constrained.quantified)), self.priority); + return Ok(Solution::Unique(constrained.quantified)); } // Otherwise, we have (positive or negative) obligations remaining, but @@ -433,15 +428,12 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let subst = self .infer .canonicalize(self.solver.program.interner(), &subst); - return ( - Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))), - self.priority, - ); + return Ok(Solution::Ambig(Guidance::Suggested(subst.quantified))); } } } - (Ok(Solution::Ambig(Guidance::Unknown)), self.priority) + Ok(Solution::Ambig(Guidance::Unknown)) } else { // While we failed to prove the goal, we still learned that // something had to hold. Here's an example where this happens: @@ -466,10 +458,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { let subst = self .infer .canonicalize(self.solver.program.interner(), &subst); - ( - Ok(Solution::Ambig(Guidance::Definite(subst.quantified))), - self.priority, - ) + Ok(Solution::Ambig(Guidance::Definite(subst.quantified))) } } diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive/mod.rs index 97564e4c685..7cb860ee441 100644 --- a/chalk-solve/src/recursive/mod.rs +++ b/chalk-solve/src/recursive/mod.rs @@ -105,7 +105,7 @@ impl<'me, I: Interner> Solver<'me, I> { debug!("solve_root_goal(canonical_goal={:?})", canonical_goal); assert!(self.context.stack.is_empty()); let minimums = &mut Minimums::new(); - self.solve_goal(canonical_goal.clone(), minimums).0 + self.solve_goal(canonical_goal.clone(), minimums) } /// Attempt to solve a goal that has been fully broken down into leaf form @@ -115,13 +115,13 @@ impl<'me, I: Interner> Solver<'me, I> { &mut self, goal: UCanonicalGoal, minimums: &mut Minimums, - ) -> (Fallible>, ClausePriority) { + ) -> Fallible> { info_heading!("solve_goal({:?})", goal); // First check the cache. if let Some(value) = self.context.cache.get(&goal) { debug!("solve_reduced_goal: cache hit, value={:?}", value); - return (value.clone(), ClausePriority::High); + return value.clone(); } // Next, check if the goal is in the search tree already. @@ -139,13 +139,10 @@ impl<'me, I: Interner> Solver<'me, I> { constraints: vec![], }; debug!("applying coinductive semantics"); - return ( - Ok(Solution::Unique(Canonical { - value, - binders: goal.canonical.binders, - })), - ClausePriority::High, - ); + return Ok(Solution::Unique(Canonical { + value, + binders: goal.canonical.binders, + })); } self.context.stack[depth].flag_cycle(); @@ -160,7 +157,7 @@ impl<'me, I: Interner> Solver<'me, I> { "solve_goal: cycle detected, previous solution {:?} with prio {:?}", previous_solution, previous_solution_priority ); - (previous_solution, previous_solution_priority) + previous_solution } else { // Otherwise, push the goal onto the stack and create a table. // The initial result for this table is error. @@ -195,7 +192,7 @@ impl<'me, I: Interner> Solver<'me, I> { } info!("solve_goal: solution = {:?} prio {:?}", result, priority); - (result, priority) + result } } @@ -345,11 +342,11 @@ impl<'me, I: Interner> Solver<'me, I> { minimums: &mut Minimums, ) -> (Fallible>, ClausePriority) { debug_heading!("solve_via_simplification({:?})", canonical_goal); - let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal, ClausePriority::High); + let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal); if let Err(e) = fulfill.push_goal(&goal.environment, goal.goal) { return (Err(e), ClausePriority::High); } - fulfill.solve(subst, minimums) + (fulfill.solve(subst, minimums), ClausePriority::High) } /// See whether we can solve a goal by implication on any of the given @@ -434,7 +431,7 @@ impl<'me, I: Interner> Solver<'me, I> { clause ); let interner = self.program.interner(); - let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal, clause.value.priority); + let (mut fulfill, subst, goal) = Fulfill::new(self, canonical_goal); let ProgramClauseImplication { consequence, conditions, @@ -455,7 +452,7 @@ impl<'me, I: Interner> Solver<'me, I> { } // and then try to solve - fulfill.solve(subst, minimums) + (fulfill.solve(subst, minimums), clause.value.priority) } fn program_clauses_for_goal( From 2316ca6c4f79bc723687e582d80637d37dc34593 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 14 Apr 2020 19:45:50 +0200 Subject: [PATCH 42/50] Remove AliasTy::type_parameters --- chalk-ir/src/lib.rs | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index b951452abfd..961e0a6ad15 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -840,15 +840,12 @@ impl AliasTy { Ty::new(interner, self) } - pub fn type_parameters<'a>(&'a self, interner: &'a I) -> impl Iterator> + 'a { + pub fn self_type_parameter(&self, interner: &I) -> Ty { self.substitution .iter(interner) - .filter_map(move |p| p.ty(interner)) - .cloned() - } - - pub fn self_type_parameter(&self, interner: &I) -> Ty { - self.type_parameters(interner).next().unwrap() + .find_map(move |p| p.ty(interner)) + .unwrap() + .clone() } } From 8fcad2f8958ea3933d69e4ffc2cc041e8c5bf7a5 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Tue, 14 Apr 2020 20:10:35 +0200 Subject: [PATCH 43/50] Address some review comments - bring back tests I commented out - add a few comments - add an is_var helper --- chalk-ir/src/lib.rs | 8 +++++++ chalk-solve/src/clauses.rs | 33 ++++++++------------------- chalk-solve/src/clauses/generalize.rs | 4 +++- tests/test/projection.rs | 32 ++++++++++++++++++-------- 4 files changed, 43 insertions(+), 34 deletions(-) diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 961e0a6ad15..0823f8d177e 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -229,6 +229,14 @@ impl Ty { } } + /// Returns true if this is a `BoundVar` or `InferenceVar`. + pub fn is_var(&self, interner: &I) -> bool { + match self.data(interner) { + TyData::BoundVar(_) | TyData::InferenceVar(_) => true, + _ => false, + } + } + pub fn is_alias(&self, interner: &I) -> bool { match self.data(interner) { TyData::Alias(..) => true, diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 7eb6041ec3c..d1b13b86596 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -233,6 +233,11 @@ fn program_clauses_that_could_match( // and `bounded_ty` is the `exists { .. }` // clauses shown above. + // Turn free BoundVars in the type into new existentials. E.g. + // we might get some `dyn Foo`, and we don't want to return + // a clause with a free variable. We can instead return a + // slightly more general clause by basically turning this into + // `exists dyn Foo`. let generalized_dyn_ty = generalize::Generalize::apply(db.interner(), dyn_ty); builder.push_binders(&generalized_dyn_ty, |builder, dyn_ty| { @@ -278,7 +283,7 @@ fn program_clauses_that_could_match( match_ty(builder, environment, ty)? } DomainGoal::FromEnv(_) => (), // Computed in the environment - DomainGoal::Normalize(Normalize { alias, ty }) => { + DomainGoal::Normalize(Normalize { alias, ty: _ }) => { // Normalize goals derive from `AssociatedTyValue` datums, // which are found in impls. That is, if we are // normalizing (e.g.) `::Item>`, then @@ -294,30 +299,12 @@ fn program_clauses_that_could_match( let trait_id = associated_ty_datum.trait_id; let trait_parameters = db.trait_parameters_from_projection(alias); - if (alias - .self_type_parameter(interner) - .bound(interner) - .is_some() - || alias - .self_type_parameter(interner) - .inference_var(interner) - .is_some()) - && (ty.bound(interner).is_some() || ty.inference_var(interner).is_some()) - { - return Err(Floundered); - } - let trait_datum = db.trait_datum(trait_id); - // FIXME - if (alias - .self_type_parameter(interner) - .bound(interner) - .is_some() - || alias - .self_type_parameter(interner) - .inference_var(interner) - .is_some()) + // Flounder if the self-type is unknown and the trait is non-enumerable. + // + // e.g., Normalize(::Item = u32) + if (alias.self_type_parameter(interner).is_var(interner)) && trait_datum.is_non_enumerable_trait() { return Err(Floundered); diff --git a/chalk-solve/src/clauses/generalize.rs b/chalk-solve/src/clauses/generalize.rs index c1babc0b95e..4ca517cd5ed 100644 --- a/chalk-solve/src/clauses/generalize.rs +++ b/chalk-solve/src/clauses/generalize.rs @@ -2,7 +2,9 @@ //! ones. We use this when building clauses that contain types passed to //! `program_clauses`; these may contain variables, and just copying those //! variables verbatim leads to problems. Instead, we return a slightly more -//! general program clause, with new variables in those places. +//! general program clause, with new variables in those places. This can only +//! happen with `dyn Trait` currently; that's the only case where we use the +//! types passed to `program_clauses` in the clauses we generate. use chalk_engine::fallible::Fallible; use chalk_ir::{ diff --git a/tests/test/projection.rs b/tests/test/projection.rs index 2be323d7594..ff3e09a013a 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -76,7 +76,6 @@ fn normalize_basic() { "Unique" } - /* TODO: this doesn't seem to be correct, actually goal { forall { if (T: Iterator) { @@ -86,10 +85,9 @@ fn normalize_basic() { } } } yields { - // True for `U = T`, of course, but also true for `U = Vec`. + // True for `U = T`, of course, but also true for `U = Vec<::Item>`. "Ambiguous" } - */ } } @@ -142,6 +140,9 @@ fn projection_equality() { exists { S: Trait2 } + } yields[SolverChoice::slg_default()] { + // this is wrong, chalk#234 + "Ambiguous" } yields[SolverChoice::recursive()] { "Unique; substitution [?0 := u32]" } @@ -167,6 +168,9 @@ fn projection_equality_from_env() { } } } + } yields[SolverChoice::slg_default()] { + // this is wrong, chalk#234 + "Ambiguous" } yields[SolverChoice::recursive()] { "Unique; substitution [?0 := u32]" } @@ -194,7 +198,10 @@ fn projection_equality_nested() { } } } - } yields[SolverChoice::recursive()] { + } yields[SolverChoice::slg_default()] { + // this is wrong, chalk#234 + "Ambiguous" + } yields[SolverChoice::recursive()] { "Unique; substitution [?0 := u32]" } } @@ -235,6 +242,9 @@ fn iterator_flatten() { } } } + } yields[SolverChoice::slg_default()] { + // this is wrong, chalk#234 + "Ambiguous" } yields[SolverChoice::recursive()] { "Unique; substitution [?0 := u32]" } @@ -536,17 +546,18 @@ fn normalize_under_binder() { } } - /* TODO: this doesn't seem to be correct, actually goal { exists { forall<'a> { Ref<'a, I32>: Deref<'a, Item = U> } } - } yields { + } yields[SolverChoice::slg_default()] { + // chalk#234, I think "Ambiguous" + } yields[SolverChoice::recursive()] { + "Unique; substitution [?0 := I32], lifetime constraints []" } - */ goal { exists { @@ -558,17 +569,18 @@ fn normalize_under_binder() { "Unique; substitution [?0 := I32], lifetime constraints []" } - /* TODO: this doesn't seem to be correct, actually goal { forall<'a> { exists { Ref<'a, I32>: Id<'a, Item = U> } } - } yields { + } yields[SolverChoice::slg_default()] { + // chalk#234, I think "Ambiguous" + } yields[SolverChoice::recursive()] { + "Unique; substitution [?0 := Ref<'!1_0, I32>], lifetime constraints []" } - */ goal { forall<'a> { From 57683759a76ed8d3fe85020bec5eb8f01a6ca098 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 14 Apr 2020 22:08:23 +0000 Subject: [PATCH 44/50] ensure all tests run for recursive solve --- tests/test/coinduction.rs | 31 ++++++++++++++++++++++++------- tests/test/misc.rs | 4 ++++ 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/tests/test/coinduction.rs b/tests/test/coinduction.rs index 16026996476..1de16427fb8 100644 --- a/tests/test/coinduction.rs +++ b/tests/test/coinduction.rs @@ -210,7 +210,15 @@ fn coinductive_unsound1() { goal { forall { X: C1orC2 } - } yields_all[SolverChoice::slg(3, None)] { + } yields[SolverChoice::slg(3, None)] { + "No possible solution" + } + + goal { + forall { X: C1orC2 } + } yields[SolverChoice::recursive()] { + // FIXME -- recursive solver doesn't handle coinduction correctly + "Unique; substitution [], lifetime constraints []" } } } @@ -251,7 +259,8 @@ fn coinductive_unsound2() { goal { forall { X: C1orC2 } - } yields_all[SolverChoice::slg(3, None)] { + } yields { + "No possible solution" } } } @@ -298,8 +307,8 @@ fn coinductive_multicycle1() { goal { forall { X: Any } - } yields_all[SolverChoice::slg(3, None)] { - "substitution [], lifetime constraints []" + } yields { + "Unique; substitution [], lifetime constraints []" } } } @@ -338,8 +347,8 @@ fn coinductive_multicycle2() { goal { forall { X: Any } - } yields_all[SolverChoice::slg(3, None)] { - "substitution [], lifetime constraints []" + } yields { + "Unique; substitution [], lifetime constraints []" } } } @@ -388,7 +397,8 @@ fn coinductive_multicycle3() { goal { forall { X: Any } - } yields_all[SolverChoice::slg(3, None)] { + } yields { + "No possible solution" } } } @@ -439,5 +449,12 @@ fn coinductive_multicycle4() { forall { X: Any } } yields_all[SolverChoice::slg(3, None)] { } + + goal { + forall { X: Any } + } yields[SolverChoice::recursive()] { + // FIXME -- recursive solver doesn't have coinduction correctly + "Unique; substitution [], lifetime constraints []" + } } } diff --git a/tests/test/misc.rs b/tests/test/misc.rs index a3d76bf00f7..7b9b172bea7 100644 --- a/tests/test/misc.rs +++ b/tests/test/misc.rs @@ -129,6 +129,8 @@ fn only_draw_so_many() { exists { T: Sized } } yields[SolverChoice::slg(10, Some(2))] { "Ambiguous; no inference guidance" + } yields[SolverChoice::recursive()] { + "Ambiguous; no inference guidance" } } } @@ -155,6 +157,8 @@ fn only_draw_so_many_blow_up() { exists { T: Foo } } yields[SolverChoice::slg(10, Some(2))] { "Ambiguous; definite substitution for { [?0 := Vec<^0.0>] }" + } yields[SolverChoice::recursive()] { + "Ambiguous; definite substitution for { [?0 := Vec<^0.0>] }" } } } From 13b66f12b8ad69d88526e1a5c9a71ee924b80c05 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 14 Apr 2020 22:09:57 +0000 Subject: [PATCH 45/50] don't silently ignore recursive solver --- tests/test/mod.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/tests/test/mod.rs b/tests/test/mod.rs index 2210dad8792..2e1f26b1a6a 100644 --- a/tests/test/mod.rs +++ b/tests/test/mod.rs @@ -230,11 +230,7 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>) { match (&solver_choice, &expected) { (SolverChoice::Recursive { .. }, TestGoal::All(_)) | (SolverChoice::Recursive { .. }, TestGoal::First(_)) => { - println!( - "skipping goal {} for recursive solver because it requires solve_multiple", - goal_text - ); - continue; + panic!("cannot test the recursive solver with yields_first or yields_all"); } _ => {} }; From 72be50072e908802247ea1d0253f259523c1eb16 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Wed, 15 Apr 2020 11:32:41 +0200 Subject: [PATCH 46/50] Move recursive module from mod.rs to recursive.rs --- chalk-solve/src/{recursive/mod.rs => recursive.rs} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename chalk-solve/src/{recursive/mod.rs => recursive.rs} (100%) diff --git a/chalk-solve/src/recursive/mod.rs b/chalk-solve/src/recursive.rs similarity index 100% rename from chalk-solve/src/recursive/mod.rs rename to chalk-solve/src/recursive.rs From a952c8771e226f98ff350286ebbd685d0174ab01 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Wed, 15 Apr 2020 09:45:06 +0000 Subject: [PATCH 47/50] add some more projection tests --- tests/test/projection.rs | 132 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 132 insertions(+) diff --git a/tests/test/projection.rs b/tests/test/projection.rs index ff3e09a013a..374a31f594f 100644 --- a/tests/test/projection.rs +++ b/tests/test/projection.rs @@ -136,6 +136,17 @@ fn projection_equality() { } } + goal { + exists { + S: Trait1 + } + } yields[SolverChoice::slg_default()] { + // this is wrong, chalk#234 + "Ambiguous" + } yields[SolverChoice::recursive()] { + "Unique; substitution [?0 := u32]" + } + goal { exists { S: Trait2 @@ -149,6 +160,127 @@ fn projection_equality() { } } +#[test] +fn projection_equality_priority1() { + test! { + program { + trait Trait1 { + type Type; + } + + struct u32 {} + struct S1 {} + struct S2 {} + struct S3 {} + + impl Trait1 for S1 { + type Type = u32; + } + } + + goal { + exists { + S1: Trait1 + } + } yields[SolverChoice::slg_default()] { + // this is wrong, chalk#234 + "Ambiguous" + } yields[SolverChoice::recursive()] { + // This is.. interesting, but not necessarily wrong. + // It's certainly true that based on the impls we see + // the only possible value for `U` is `u32`. + // + // Can we come to any harm by inferring that `T = S2` + // here, even though we could've chosen to say that + // `U = !>::Type` and thus not + // constrained `T` at all? I can't come up with + // an example where that's the case, so maybe + // not. -Niko + "Unique; substitution [?0 := S2, ?1 := u32]" + } + } +} + +#[test] +fn projection_equality_priority2() { + test! { + program { + trait Trait1 { + type Type; + } + + struct u32 {} + struct S1 {} + struct S2 {} + struct S3 {} + + impl Trait1 for X { + type Type = u32; + } + } + + goal { + forall { + if (X: Trait1) { + exists { + X: Trait1 + } + } + } + } yields { + // Correct: Ambiguous because Out1 = Y and Out1 = S1 are both value. + "Ambiguous; no inference guidance" + } + + goal { + forall { + if (X: Trait1) { + exists { + X: Trait1, + Out1 = Y + } + } + } + } yields { + // Constraining Out1 = Y gives us only one choice. + "Unique; substitution [?0 := !1_1, ?1 := (Trait1::Type)], lifetime constraints []" + } + + goal { + forall { + if (X: Trait1) { + exists { + Out1 = Y, + X: Trait1 + } + } + } + } yields { + // Constraining Out1 = Y gives us only one choice. + "Unique; substitution [?0 := !1_1, ?1 := (Trait1::Type)], lifetime constraints []" + } + + goal { + forall { + if (X: Trait1) { + exists { + Out1 = S1, + X: Trait1 + } + } + } + } yields[SolverChoice::slg_default()] { + // chalk#234: Constraining Out1 = S1 gives us only the choice to + // use the impl, but the SLG solver can't decide between + // the placeholder and the normalized form. + "Ambiguous; definite substitution for { [?0 := S1, ?1 := ^0.0] }" + } yields[SolverChoice::recursive()] { + // Constraining Out1 = S1 gives us only one choice, use the impl, + // and the recursive solver prefers the normalized form. + "Unique; substitution [?0 := S1, ?1 := u32], lifetime constraints []" + } + } +} #[test] fn projection_equality_from_env() { test! { From 77f262f3fd26402f9ac37831932fd1bd4be68fa8 Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Wed, 15 Apr 2020 19:51:20 +0200 Subject: [PATCH 48/50] Rebase fixes; flounder instead of truncating, like SLG --- chalk-solve/src/clauses/generalize.rs | 5 +---- chalk-solve/src/recursive.rs | 10 +++++----- chalk-solve/src/recursive/fulfill.rs | 28 ++++++++++++++++++++------- chalk-solve/src/solve/slg.rs | 3 +-- tests/test/cycle.rs | 6 +----- 5 files changed, 29 insertions(+), 23 deletions(-) diff --git a/chalk-solve/src/clauses/generalize.rs b/chalk-solve/src/clauses/generalize.rs index 4ca517cd5ed..0bfb0250874 100644 --- a/chalk-solve/src/clauses/generalize.rs +++ b/chalk-solve/src/clauses/generalize.rs @@ -30,10 +30,7 @@ impl Generalize<'_, I> { let value = value .fold_with(&mut generalize, DebruijnIndex::INNERMOST) .unwrap(); - Binders { - binders: generalize.binders, - value, - } + Binders::new(generalize.binders, value) } } diff --git a/chalk-solve/src/recursive.rs b/chalk-solve/src/recursive.rs index 7cb860ee441..9d03242f346 100644 --- a/chalk-solve/src/recursive.rs +++ b/chalk-solve/src/recursive.rs @@ -369,10 +369,7 @@ impl<'me, I: Interner> Solver<'me, I> { ProgramClauseData::Implies(implication) => { let res = self.solve_via_implication( canonical_goal, - &Binders { - binders: vec![], - value: implication.clone(), - }, + &Binders::new(vec![], implication.clone()), minimums, ); if let (Ok(solution), priority) = res { @@ -452,7 +449,10 @@ impl<'me, I: Interner> Solver<'me, I> { } // and then try to solve - (fulfill.solve(subst, minimums), clause.value.priority) + ( + fulfill.solve(subst, minimums), + clause.skip_binders().priority, + ) } fn program_clauses_for_goal( diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs index 7f2b3008c67..e401f6955ca 100644 --- a/chalk-solve/src/recursive/fulfill.rs +++ b/chalk-solve/src/recursive/fulfill.rs @@ -119,16 +119,30 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> { fn push_obligation(&mut self, obligation: Obligation) { // truncate to avoid overflows - let obligation = match obligation { + match &obligation { Obligation::Prove(goal) => { - let truncated = - truncate::truncate(self.solver.program.interner(), &mut self.infer, 30, &goal); - Obligation::Prove(truncated.value) + if truncate::needs_truncation( + self.solver.program.interner(), + &mut self.infer, + 30, + goal, + ) { + // the goal is too big. Record that we should return Ambiguous + self.cannot_prove = true; + return; + } } Obligation::Refute(goal) => { - let truncated = - truncate::truncate(self.solver.program.interner(), &mut self.infer, 30, &goal); - Obligation::Refute(truncated.value) + if truncate::needs_truncation( + self.solver.program.interner(), + &mut self.infer, + 30, + goal, + ) { + // the goal is too big. Record that we should return Ambiguous + self.cannot_prove = true; + return; + } } }; self.obligations.push(obligation); diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs index 33d90338bd9..c23eea490e3 100644 --- a/chalk-solve/src/solve/slg.rs +++ b/chalk-solve/src/solve/slg.rs @@ -14,8 +14,7 @@ use chalk_engine::hh::HhGoal; use chalk_engine::{CompleteAnswer, ExClause, Literal}; use chalk_ir::cast::Cast; use chalk_ir::cast::Caster; -use chalk_ir::could_match::CouldMatch; -use chalk_ir::interner::{HasInterner, Interner}; +use chalk_ir::interner::Interner; use chalk_ir::*; use std::fmt::Debug; diff --git a/tests/test/cycle.rs b/tests/test/cycle.rs index 3e2a008cd9d..ebf097ea6f8 100644 --- a/tests/test/cycle.rs +++ b/tests/test/cycle.rs @@ -165,12 +165,8 @@ fn overflow() { S: Q } yields[SolverChoice::slg(10, None)] { "Ambiguous; no inference guidance" - } - - goal { - S: Q } yields[SolverChoice::recursive()] { - "No possible solution" + "Ambiguous; no inference guidance" } } } From b032df6edb6deca339f6d571032059b3ef6837cd Mon Sep 17 00:00:00 2001 From: Florian Diebold Date: Wed, 15 Apr 2020 20:06:07 +0200 Subject: [PATCH 49/50] Use combine_with_priorities when combining answers from cycles as well --- chalk-solve/src/recursive.rs | 73 +++++++++++++++++++++++------------- 1 file changed, 47 insertions(+), 26 deletions(-) diff --git a/chalk-solve/src/recursive.rs b/chalk-solve/src/recursive.rs index 9d03242f346..fd6a8e57927 100644 --- a/chalk-solve/src/recursive.rs +++ b/chalk-solve/src/recursive.rs @@ -294,6 +294,18 @@ impl<'me, I: Interner> Solver<'me, I> { return *minimums; } + let old_answer = &self.context.search_graph[dfn].solution; + let old_prio = self.context.search_graph[dfn].solution_priority; + + let (current_answer, current_prio) = combine_with_priorities_for_goal( + self.program.interner(), + &canonical_goal.canonical.value.goal, + old_answer.clone(), + old_prio, + current_answer, + current_prio, + ); + // Some of our subgoals depended on us. We need to re-run // with the current answer. if self.context.search_graph[dfn].solution == current_answer { @@ -301,21 +313,6 @@ impl<'me, I: Interner> Solver<'me, I> { return *minimums; } - if ( - self.context.search_graph[dfn].solution_priority, - current_prio, - ) == (ClausePriority::High, ClausePriority::Low) - && self.context.search_graph[dfn].solution.is_ok() - { - // TODO check solution inputs? - // Not replacing the current answer, so we're at a fixed point? - debug!( - "solve_new_subgoal: new answer has lower priority (old answer: {:?})", - self.context.search_graph[dfn].solution - ); - return *minimums; - } - let current_answer_is_ambig = match ¤t_answer { Ok(s) => s.is_ambig(), Err(_) => false, @@ -378,7 +375,7 @@ impl<'me, I: Interner> Solver<'me, I> { None => (solution, priority), Some((cur, cur_priority)) => combine_with_priorities( self.program.interner(), - canonical_goal, + &canonical_goal.canonical.value.goal, cur, cur_priority, solution, @@ -397,7 +394,7 @@ impl<'me, I: Interner> Solver<'me, I> { None => (solution, priority), Some((cur, cur_priority)) => combine_with_priorities( self.program.interner(), - canonical_goal, + &canonical_goal.canonical.value.goal, cur, cur_priority, solution, @@ -466,23 +463,47 @@ impl<'me, I: Interner> Solver<'me, I> { fn calculate_inputs( interner: &I, - canonical_goal: &UCanonical>>, + domain_goal: &DomainGoal, solution: &Solution, ) -> Vec> { if let Some(subst) = solution.constrained_subst() { - let subst_goal = subst - .value - .subst - .apply(&canonical_goal.canonical.value.goal, interner); + let subst_goal = subst.value.subst.apply(&domain_goal, interner); subst_goal.inputs(interner) } else { - canonical_goal.canonical.value.goal.inputs(interner) + domain_goal.inputs(interner) + } +} + +fn combine_with_priorities_for_goal( + interner: &I, + goal: &Goal, + a: Fallible>, + prio_a: ClausePriority, + b: Fallible>, + prio_b: ClausePriority, +) -> (Fallible>, ClausePriority) { + let domain_goal = match goal.data(interner) { + GoalData::DomainGoal(domain_goal) => domain_goal, + _ => { + // non-domain goals currently have no priorities, so we always take the new solution here + return (b, prio_b); + } + }; + match (a, b) { + (Ok(a), Ok(b)) => { + let (solution, prio) = + combine_with_priorities(interner, domain_goal, a, prio_a, b, prio_b); + (Ok(solution), prio) + } + (Ok(solution), Err(_)) => (Ok(solution), prio_a), + (Err(_), Ok(solution)) => (Ok(solution), prio_b), + (Err(_), Err(e)) => (Err(e), prio_b), } } fn combine_with_priorities( interner: &I, - canonical_goal: &UCanonical>>, + domain_goal: &DomainGoal, a: Solution, prio_a: ClausePriority, b: Solution, @@ -491,8 +512,8 @@ fn combine_with_priorities( match (prio_a, prio_b, a, b) { (ClausePriority::High, ClausePriority::Low, higher, lower) | (ClausePriority::Low, ClausePriority::High, lower, higher) => { - let inputs_higher = calculate_inputs(interner, canonical_goal, &higher); - let inputs_lower = calculate_inputs(interner, canonical_goal, &lower); + let inputs_higher = calculate_inputs(interner, domain_goal, &higher); + let inputs_lower = calculate_inputs(interner, domain_goal, &lower); if inputs_higher == inputs_lower { debug!( "preferring solution: {:?} over {:?} because of higher prio", From 2aa90be07d7701904b211872dfc783d035c1b462 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Wed, 15 Apr 2020 21:38:23 +0000 Subject: [PATCH 50/50] cite chalk#399 in the fixme --- tests/test/coinduction.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/test/coinduction.rs b/tests/test/coinduction.rs index 1de16427fb8..27cb65b5ec7 100644 --- a/tests/test/coinduction.rs +++ b/tests/test/coinduction.rs @@ -217,7 +217,7 @@ fn coinductive_unsound1() { goal { forall { X: C1orC2 } } yields[SolverChoice::recursive()] { - // FIXME -- recursive solver doesn't handle coinduction correctly + // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly "Unique; substitution [], lifetime constraints []" } } @@ -453,7 +453,7 @@ fn coinductive_multicycle4() { goal { forall { X: Any } } yields[SolverChoice::recursive()] { - // FIXME -- recursive solver doesn't have coinduction correctly + // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly "Unique; substitution [], lifetime constraints []" } }