Merge pull request #45 from scalexm/cannot-prove

Add `CannotProve` solution

Author: nikomatsakis

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<InEnvironment<Constraint>>,
 
     /// 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<T>(&mut self, environment: &Arc<Environment>, a: &T, b: &T) -> Result<UnifyOutcome>
+    pub fn unify<T>(&mut self, environment: &Arc<Environment>, 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,24 +311,30 @@ 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)
                     }
                 };
 
                 if ambiguous {
                     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<Solution> {
         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.
 

src/solve/infer/unify.rs

@@ -34,7 +34,7 @@ struct Unifier<'t> {
     snapshot: InferenceSnapshot,
     goals: Vec<InEnvironment<LeafGoal>>,
     constraints: Vec<InEnvironment<Constraint>>,
-    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> { T = U } // Ambig
-                        //     forall<T, U> { not { T = U } } // Ambig
+                        //     forall<T, U> { T = U } // CannotProve
+                        //     forall<T, U> { not { T = U } } // CannotProve
 
-                        self.ambiguous = true;
+                        self.cannot_prove = true;
                         return Ok(())
                     } else {
                         bail!("cannot equate `{:?}` and `{:?}`", apply1.name, apply2.name);

src/solve/mod.rs

@@ -16,11 +16,16 @@ pub enum Solution {
     /// which must also hold for the goal to be valid.
     Unique(Canonical<ConstrainedSubst>),
 
-    /// 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")
+            }
         }
     }
 }

src/solve/solver.rs

@@ -115,21 +115,21 @@ 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
                 let fallback: Vec<_> = self.program.program_clauses.iter()
                     .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<UniverseIndex>],
         goal: &InEnvironment<DomainGoal>,
-        clauses: C,
-        from_env: bool,
+        clauses: C
     ) -> Result<Solution>
     where
         C: IntoIterator<Item = ProgramClause>,
@@ -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<UniverseIndex>],
         goal: InEnvironment<DomainGoal>,
-        clause: Binders<ProgramClauseImplication>,
-        from_env: bool,
+        clause: Binders<ProgramClauseImplication>
     ) -> Result<Solution> {
         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<T> { }
-            //
-            //     impl<T> Foo<i32> for T { }
-            // }
-            //
-            // goal {
-            //     forall<T> {
-            //         exists<U> {
-            //             if (i32: Foo<T>) {
-            //                 T: Foo<U>
-            //             }
-            //         }
-            //     }
-            // } 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 {