diff --git a/src/solve/fulfill.rs b/src/solve/fulfill.rs index f8adb8faa58..9e1335af4f7 100644 --- a/src/solve/fulfill.rs +++ b/src/solve/fulfill.rs @@ -23,10 +23,6 @@ impl Outcome { } } -pub struct UnifyOutcome { - pub ambiguous: bool, -} - /// A goal that must be resolved #[derive(Clone, Debug, PartialEq, Eq)] enum Obligation { @@ -53,6 +49,7 @@ struct PositiveSolution { enum NegativeSolution { Refuted, Ambiguous, + CannotProve, } /// A `Fulfill` is where we actually break down complex goals, instantiate @@ -77,8 +74,9 @@ pub struct Fulfill<'s> { constraints: HashSet>, /// Record that a goal has been processed that can neither be proved nor - /// refuted, and thus the overall solution cannot be `Unique` - ambiguous: bool, + /// 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> { @@ -88,7 +86,7 @@ impl<'s> Fulfill<'s> { infer: InferenceTable::new(), obligations: vec![], constraints: HashSet::new(), - ambiguous: false, + cannot_prove: false, } } @@ -119,19 +117,19 @@ impl<'s> Fulfill<'s> { /// /// Wraps `InferenceTable::unify`; any resulting normalizations are added /// into our list of pending obligations with the given environment. - pub fn unify(&mut self, environment: &Arc, a: &T, b: &T) -> Result + pub fn unify(&mut self, environment: &Arc, a: &T, b: &T) -> Result<()> where T: ?Sized + Zip + Debug { - let UnificationResult { goals, constraints, ambiguous } = + let UnificationResult { goals, constraints, cannot_prove } = self.infer.unify(environment, a, b)?; debug!("unify({:?}, {:?}) succeeded", a, b); debug!("unify: goals={:?}", goals); debug!("unify: constraints={:?}", constraints); - debug!("unify: ambiguous={:?}", ambiguous); + debug!("unify: cannot_prove={:?}", cannot_prove); self.constraints.extend(constraints); self.obligations.extend(goals.into_iter().map(Obligation::Prove)); - self.ambiguous = self.ambiguous || ambiguous; - Ok(UnifyOutcome { ambiguous }) + self.cannot_prove = self.cannot_prove || cannot_prove; + Ok(()) } /// Create obligations for the given goal in the given environment. This may @@ -223,10 +221,11 @@ impl<'s> Fulfill<'s> { } // Negate the result - if let Ok(solution) = self.solver.solve_closed_goal(canonicalized.quantified.value) { + if let Ok(solution) = self.solver.solve_closed_goal(canonicalized.quantified.value) { match solution { Solution::Unique(_) => Err("refutation failed")?, Solution::Ambig(_) => Ok(NegativeSolution::Ambiguous), + Solution::CannotProve => Ok(NegativeSolution::CannotProve), } } else { Ok(NegativeSolution::Refuted) @@ -301,7 +300,7 @@ impl<'s> Fulfill<'s> { // directly. assert!(obligations.is_empty()); while let Some(obligation) = self.obligations.pop() { - let ambiguous = match obligation { + let (ambiguous, cannot_prove) = match obligation { Obligation::Prove(ref wc) => { let PositiveSolution { free_vars, solution } = self.prove(wc)?; @@ -312,10 +311,11 @@ impl<'s> Fulfill<'s> { } } - solution.is_ambig() + (solution.is_ambig(), solution.cannot_be_proven()) } Obligation::Refute(ref goal) => { - self.refute(goal)? == NegativeSolution::Ambiguous + let answer = self.refute(goal)?; + (answer == NegativeSolution::Ambiguous, answer == NegativeSolution::CannotProve) } }; @@ -323,13 +323,18 @@ impl<'s> Fulfill<'s> { debug!("ambiguous result: {:?}", obligation); obligations.push(obligation); } + + // If one of the obligations cannot be proven then the whole goal + // cannot be proven either, unless another obligation leads to an error + // in which case the function will bail out normally. + self.cannot_prove = self.cannot_prove || cannot_prove; } self.obligations.extend(obligations.drain(..)); debug!("end of round, {} obligations left", self.obligations.len()); } - // At the end of this process, `self.to_prove` should have + // At the end of this process, `self.obligations` should have // all of the ambiguous obligations, and `obligations` should // be empty. assert!(obligations.is_empty()); @@ -346,7 +351,12 @@ impl<'s> Fulfill<'s> { /// the outcome of type inference by updating the replacements it provides. pub fn solve(mut self, subst: Substitution) -> Result { let outcome = self.fulfill()?; - if outcome.is_complete() && !self.ambiguous { + + if self.cannot_prove { + return Ok(Solution::CannotProve); + } + + 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. diff --git a/src/solve/infer/unify.rs b/src/solve/infer/unify.rs index f3a5a7f5f31..bc13621e396 100644 --- a/src/solve/infer/unify.rs +++ b/src/solve/infer/unify.rs @@ -34,7 +34,7 @@ struct Unifier<'t> { snapshot: InferenceSnapshot, goals: Vec>, constraints: Vec>, - ambiguous: bool, + cannot_prove: bool, } #[derive(Debug)] @@ -46,7 +46,7 @@ pub struct UnificationResult { /// neither confirm nor deny their equality, since we interpret the /// unification request as talking about *all possible /// substitutions*. Instead, we return an ambiguous result. - pub ambiguous: bool, + pub cannot_prove: bool, } impl<'t> Unifier<'t> { @@ -58,7 +58,7 @@ impl<'t> Unifier<'t> { snapshot: snapshot, goals: vec![], constraints: vec![], - ambiguous: false, + cannot_prove: false, } } @@ -67,7 +67,7 @@ impl<'t> Unifier<'t> { Ok(UnificationResult { goals: self.goals, constraints: self.constraints, - ambiguous: self.ambiguous, + cannot_prove: self.cannot_prove, }) } @@ -118,13 +118,13 @@ impl<'t> Unifier<'t> { if apply1.name.is_for_all() || apply2.name.is_for_all() { // we're being asked to prove something like `!0 = !1` // or `!0 = i32`. We interpret this as being asked - // whether that holds *for all subtitutions*. Thus, the - // answer is always *maybe* (ambiguous). That means we get: + // whether that holds *for all subtitutions*. Thus, we + // cannot prove the goal. That means we get: // - // forall { T = U } // Ambig - // forall { not { T = U } } // Ambig + // forall { T = U } // CannotProve + // forall { not { T = U } } // CannotProve - self.ambiguous = true; + self.cannot_prove = true; return Ok(()) } else { bail!("cannot equate `{:?}` and `{:?}`", apply1.name, apply2.name); diff --git a/src/solve/mod.rs b/src/solve/mod.rs index a0d33fdd4cc..c3d4979d89d 100644 --- a/src/solve/mod.rs +++ b/src/solve/mod.rs @@ -16,11 +16,16 @@ pub enum Solution { /// which must also hold for the goal to be valid. Unique(Canonical), - /// The goal may or may not hold, but regardless we may have some guidance + /// The goal may be provable in multiple ways, but regardless we may have some guidance /// for type inference. In this case, we don't return any lifetime /// constraints, since we have not "committed" to any particular solution /// yet. Ambig(Guidance), + + /// There is no instantiation of the existentials for which we could prove this goal + /// to be true. Nonetheless, the goal may yet be true for some instantiations of the + /// universals. In other words, this goal is neither true nor false. + CannotProve, } #[derive(Clone, Debug, PartialEq, Eq)] @@ -66,8 +71,8 @@ impl Solution { use self::Guidance::*; if self == other { return self } - if self.is_empty_unique() { return self } - if other.is_empty_unique() { return other } + if other.cannot_be_proven() { return self } + if self.cannot_be_proven() { return other } // Otherwise, always downgrade to Ambig: @@ -93,8 +98,8 @@ impl Solution { use self::Guidance::*; if self == other { return self } - if self.is_empty_unique() { return self } - if other.is_empty_unique() { return other } + if other.cannot_be_proven() { return self } + if self.cannot_be_proven() { return other } // Otherwise, always downgrade to Ambig: @@ -113,6 +118,9 @@ impl Solution { use self::Guidance::*; if self == other { return self } + if other.cannot_be_proven() { return self } + if self.cannot_be_proven() { return other } + if let Solution::Ambig(guidance) = self { match guidance { Definite(subst) | Suggested(subst) => Solution::Ambig(Suggested(subst)), @@ -132,7 +140,8 @@ impl Solution { binders: constrained.binders, }) } - Solution::Ambig(guidance) => guidance + Solution::Ambig(guidance) => guidance, + Solution::CannotProve => Guidance::Unknown, } } @@ -148,7 +157,7 @@ impl Solution { }; Some(Canonical { value, binders: canonical.binders.clone() }) } - Solution::Ambig(_) => None, + Solution::Ambig(_) | Solution::CannotProve => None, } } @@ -169,13 +178,9 @@ impl Solution { } } - /// We use emptiness, rather than triviality, to deduce that alternative - /// solutions **cannot meaningfully differ** - pub fn is_empty_unique(&self) -> bool { + pub fn cannot_be_proven(&self) -> bool { match *self { - Solution::Unique(ref subst) => { - subst.binders.is_empty() && subst.value.subst.is_empty() - } + Solution::CannotProve => true, _ => false, } } @@ -198,6 +203,9 @@ impl fmt::Display for Solution { Solution::Ambig(Guidance::Unknown) => { write!(f, "Ambiguous; no inference guidance") } + Solution::CannotProve => { + write!(f, "CannotProve") + } } } } diff --git a/src/solve/solver.rs b/src/solve/solver.rs index 210a79615e3..f5238e8d1a7 100644 --- a/src/solve/solver.rs +++ b/src/solve/solver.rs @@ -115,13 +115,13 @@ impl Solver { .environment .elaborated_clauses(&self.program) .map(DomainGoal::into_program_clause); - let env_solution = self.solve_from_clauses(&binders, &value, env_clauses, true); + let env_solution = self.solve_from_clauses(&binders, &value, env_clauses); let prog_clauses: Vec<_> = self.program.program_clauses.iter() .cloned() .filter(|clause| !clause.fallback_clause) .collect(); - let prog_solution = self.solve_from_clauses(&binders, &value, prog_clauses, false); + let prog_solution = self.solve_from_clauses(&binders, &value, prog_clauses); // These fallback clauses are used when we're sure we'll never // reach Unique via another route @@ -129,7 +129,7 @@ impl Solver { .cloned() .filter(|clause| clause.fallback_clause) .collect(); - let fallback_solution = self.solve_from_clauses(&binders, &value, fallback, false); + let fallback_solution = self.solve_from_clauses(&binders, &value, fallback); // Now that we have all the outcomes, we attempt to combine // them. Here, we apply a heuristic (also found in rustc): if we @@ -172,8 +172,7 @@ impl Solver { &mut self, binders: &[ParameterKind], goal: &InEnvironment, - clauses: C, - from_env: bool, + clauses: C ) -> Result where C: IntoIterator, @@ -182,7 +181,7 @@ impl Solver { for ProgramClause { implication, .. } in clauses { debug_heading!("clause={:?}", implication); - let res = self.solve_via_implication(binders, goal.clone(), implication, from_env); + let res = self.solve_via_implication(binders, goal.clone(), implication); if let Ok(solution) = res { debug!("ok: solution={:?}", solution); cur_solution = Some( @@ -203,8 +202,7 @@ impl Solver { &mut self, binders: &[ParameterKind], goal: InEnvironment, - clause: Binders, - from_env: bool, + clause: Binders ) -> Result { let mut fulfill = Fulfill::new(self); let subst = Substitution::from_binders(&binders); @@ -213,42 +211,7 @@ impl Solver { let ProgramClauseImplication { consequence, conditions} = fulfill.instantiate_in(goal.environment.universe, clause.binders, &clause.value); - // first, see if the implication's conclusion might solve our goal - if fulfill.unify(&goal.environment, &goal.goal, &consequence)?.ambiguous && from_env { - // here, using this environmental assumption would require unifying a skolemized - // variable, which can only appear in an *environment*, never the - // program. We view the program as providing a "closed world" of - // possible types and impls, and thus we can safely abandon this - // route of proving our goal. - // - // You can see this at work in the following example, where the - // assumption in the `if` is ignored since it cannot actually be applied. - // - // ``` - // program { - // struct i32 { } - // struct u32 { } - // - // trait Foo { } - // - // impl Foo for T { } - // } - // - // goal { - // forall { - // exists { - // if (i32: Foo) { - // T: Foo - // } - // } - // } - // } yields { - // "Unique" - // } - // ``` - - Err("using the implication would require changing a forall variable")?; - } + fulfill.unify(&goal.environment, &goal.goal, &consequence)?; // if so, toss in all of its premises for condition in conditions { diff --git a/src/solve/test.rs b/src/solve/test.rs index a075adc8d3b..f07da7211a8 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -142,7 +142,13 @@ fn prove_forall() { goal { forall { T: Marker } } yields { - "Ambiguous; no inference guidance" + "CannotProve" + } + + goal { + forall { not { T: Marker } } + } yields { + "CannotProve" } // If we assume `T: Marker`, then obviously `T: Marker`. @@ -165,7 +171,7 @@ fn prove_forall() { goal { forall { Vec: Clone } } yields { - "Ambig" + "CannotProve" } // Here, we do know that `T: Clone`, so we can. @@ -288,7 +294,7 @@ fn normalize_basic() { } } } yields { - "Ambiguous; suggested substitution [?0 := u32]" + "Unique; substitution [?0 := u32]" } goal { @@ -1168,7 +1174,7 @@ fn negation_quantifiers() { } } } yields { - "Ambig" + "CannotProve" } goal { @@ -1188,7 +1194,7 @@ fn negation_quantifiers() { } } } yields { - "Ambig" + "CannotProve" } } }