Merge pull request #527 from nathanwhit/add-region-constraints

Refactor `LifetimeOutlives` goals to produce `AddRegionConstraint` subgoals

Author: nikomatsakis

book/src/clauses/type_equality.md

@@ -145,16 +145,15 @@ with unification. As described in the
 section, unification is basically a procedure with a signature like this:
 
 ```text
-Unify(A, B) = Result<(Subgoals, RegionConstraints), NoSolution>
+Unify(A, B) = Result<Subgoals, NoSolution>
 ```
 
 In other words, we try to unify two things A and B. That procedure
 might just fail, in which case we get back `Err(NoSolution)`. This
 would happen, for example, if we tried to unify `u32` and `i32`.
 
 The key point is that, on success, unification can also give back to
-us a set of subgoals that still remain to be proven. (It can also give
-back region constraints, but those are not relevant here).
+us a set of subgoals that still remain to be proven.
 
 Whenever unification encounters a non-placeholder associated type
 projection P being equated with some other type T, it always succeeds,

chalk-engine/src/logic.rs

@@ -12,8 +12,8 @@ use crate::{
 
 use chalk_ir::interner::Interner;
 use chalk_ir::{
-    Canonical, ConstrainedSubst, DomainGoal, Floundered, Goal, GoalData, InEnvironment, NoSolution,
-    Substitution, UCanonical, UniverseMap, WhereClause,
+    Canonical, ConstrainedSubst, Floundered, Goal, GoalData, InEnvironment, NoSolution,
+    Substitution, UCanonical, UniverseMap,
 };
 use tracing::{debug, debug_span, info, instrument};
 
@@ -251,16 +251,8 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
         let (mut infer, subst, environment, goal) = context.instantiate_ucanonical_goal(&goal);
         let goal_data = goal.data(context.interner());
 
-        let is_outlives_goal = |dg: &DomainGoal<I>| {
-            if let DomainGoal::Holds(WhereClause::LifetimeOutlives(_)) = dg {
-                true
-            } else {
-                false
-            }
-        };
-
         match goal_data {
-            GoalData::DomainGoal(domain_goal) if !is_outlives_goal(domain_goal) => {
+            GoalData::DomainGoal(domain_goal) => {
                 match context.program_clauses(&environment, &domain_goal, &mut infer) {
                     Ok(clauses) => {
                         for clause in clauses {

chalk-engine/src/simplify.rs

@@ -4,8 +4,7 @@ use crate::{ExClause, Literal, TimeStamp};
 
 use chalk_ir::interner::Interner;
 use chalk_ir::{
-    Constraint, DomainGoal, Environment, Fallible, Goal, GoalData, InEnvironment, LifetimeOutlives,
-    QuantifierKind, Substitution, WhereClause,
+    Constraint, Environment, Fallible, Goal, GoalData, InEnvironment, QuantifierKind, Substitution,
 };
 use tracing::debug;
 
@@ -69,22 +68,17 @@ impl<I: Interner, C: Context<I>> Forest<I, C> {
                     &goal.b,
                     &mut ex_clause,
                 )?,
-                GoalData::DomainGoal(domain_goal) => match domain_goal {
-                    DomainGoal::Holds(WhereClause::LifetimeOutlives(LifetimeOutlives { a, b })) => {
-                        ex_clause.constraints.push(InEnvironment::new(
+                GoalData::AddRegionConstraint(a, b) => ex_clause.constraints.push(
+                    InEnvironment::new(&environment, Constraint::Outlives(a.clone(), b.clone())),
+                ),
+                GoalData::DomainGoal(domain_goal) => {
+                    ex_clause
+                        .subgoals
+                        .push(Literal::Positive(InEnvironment::new(
                             &environment,
-                            Constraint::Outlives(a.clone(), b.clone()),
-                        ));
-                    }
-                    _ => {
-                        ex_clause
-                            .subgoals
-                            .push(Literal::Positive(InEnvironment::new(
-                                &environment,
-                                context.into_goal(domain_goal.clone()),
-                            )));
-                    }
-                },
+                            context.into_goal(domain_goal.clone()),
+                        )));
+                }
                 GoalData::CannotProve(()) => {
                     debug!("Marking Strand as ambiguous because of a `CannotProve` subgoal");
                     ex_clause.ambiguous = true;

chalk-ir/src/debug.rs

@@ -326,6 +326,9 @@ impl<I: Interner> Debug for GoalData<I> {
             GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
             GoalData::EqGoal(ref wc) => write!(fmt, "{:?}", wc),
             GoalData::DomainGoal(ref wc) => write!(fmt, "{:?}", wc),
+            GoalData::AddRegionConstraint(ref a, ref b) => {
+                write!(fmt, "AddRegionConstraint({:?}: {:?})", a, b)
+            }
             GoalData::CannotProve(()) => write!(fmt, r"¯\_(ツ)_/¯"),
         }
     }

chalk-ir/src/lib.rs

@@ -2445,6 +2445,9 @@ pub enum GoalData<I: Interner> {
     /// proven via program clauses
     DomainGoal(DomainGoal<I>),
 
+    /// Adds a region constraint requiring `'a : 'b`, given two lifetimes `'a, 'b`
+    AddRegionConstraint(Lifetime<I>, Lifetime<I>),
+
     /// Indicates something that cannot be proven to be true or false
     /// definitively. This can occur with overflow but also with
     /// unifications of skolemized variables like `forall<X,Y> { X = Y

chalk-solve/src/clauses.rs

@@ -312,7 +312,15 @@ fn program_clauses_that_could_match<I: Interner>(
                 .opaque_ty_data(opaque_ty.opaque_ty_id)
                 .to_program_clauses(builder),
         },
-        DomainGoal::Holds(WhereClause::LifetimeOutlives(_)) => {}
+        DomainGoal::Holds(WhereClause::LifetimeOutlives(LifetimeOutlives { a, b })) => {
+            builder.push_clause(
+                WhereClause::LifetimeOutlives(LifetimeOutlives {
+                    a: a.clone(),
+                    b: b.clone(),
+                }),
+                Some(GoalData::AddRegionConstraint(a.clone(), b.clone()).intern(interner)),
+            );
+        }
         DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
         | DomainGoal::LocalImplAllowed(trait_ref) => {
             db.trait_datum(trait_ref.trait_id)

chalk-solve/src/infer/test.rs

@@ -292,27 +292,26 @@ fn lifetime_constraint_indirect() {
     // '!1.
     let t_a = ty!(apply (item 0) (lifetime (placeholder 1)));
     let t_b = ty!(apply (item 0) (lifetime (infer 1)));
-    let UnificationResult { goals, constraints } =
-        table.unify(interner, &environment0, &t_a, &t_b).unwrap();
+    let UnificationResult { goals } = table.unify(interner, &environment0, &t_a, &t_b).unwrap();
     assert!(goals.is_empty());
-    assert!(constraints.is_empty());
 
     // Here, we try to unify `?0` (the type variable in universe 0)
     // with something that involves `'?1`. Since `'?1` has been
     // unified with `'!1`, and `'!1` is not visible from universe 0,
     // we will replace `'!1` with a new variable `'?2` and introduce a
     // (likely unsatisfiable) constraint relating them.
     let t_c = ty!(infer 0);
-    let UnificationResult { goals, constraints } =
-        table.unify(interner, &environment0, &t_c, &t_b).unwrap();
-    assert!(goals.is_empty());
-    assert_eq!(constraints.len(), 2);
+    let goals = table
+        .unify(interner, &environment0, &t_c, &t_b)
+        .unwrap()
+        .goals;
+    assert_eq!(goals.len(), 2);
     assert_eq!(
-        format!("{:?}", constraints[0]),
-        "InEnvironment { environment: Env([]), goal: \'?2: \'!1_0 }",
+        format!("{:?}", goals[0]),
+        "InEnvironment { environment: Env([]), goal: AddRegionConstraint(\'!1_0: \'?2) }",
     );
     assert_eq!(
-        format!("{:?}", constraints[1]),
-        "InEnvironment { environment: Env([]), goal: \'!1_0: \'?2 }",
+        format!("{:?}", goals[1]),
+        "InEnvironment { environment: Env([]), goal: AddRegionConstraint(\'?2: \'!1_0) }",
     );
 }

chalk-solve/src/infer/unify.rs

@@ -37,15 +37,13 @@ impl<I: Interner> InferenceTable<I> {
 struct Unifier<'t, I: Interner> {
     table: &'t mut InferenceTable<I>,
     environment: &'t Environment<I>,
-    goals: Vec<InEnvironment<DomainGoal<I>>>,
-    constraints: Vec<InEnvironment<Constraint<I>>>,
+    goals: Vec<InEnvironment<Goal<I>>>,
     interner: &'t I,
 }
 
 #[derive(Debug)]
 pub(crate) struct UnificationResult<I: Interner> {
-    pub(crate) goals: Vec<InEnvironment<DomainGoal<I>>>,
-    pub(crate) constraints: Vec<InEnvironment<Constraint<I>>>,
+    pub(crate) goals: Vec<InEnvironment<Goal<I>>>,
 }
 
 impl<'t, I: Interner> Unifier<'t, I> {
@@ -58,7 +56,6 @@ impl<'t, I: Interner> Unifier<'t, I> {
             environment: environment,
             table: table,
             goals: vec![],
-            constraints: vec![],
             interner,
         }
     }
@@ -71,10 +68,7 @@ impl<'t, I: Interner> Unifier<'t, I> {
         T: ?Sized + Zip<I>,
     {
         Zip::zip_with(&mut self, a, b)?;
-        Ok(UnificationResult {
-            goals: self.goals,
-            constraints: self.constraints,
-        })
+        Ok(UnificationResult { goals: self.goals })
     }
 
     fn unify_ty_ty(&mut self, a: &Ty<I>, b: &Ty<I>) -> Fallible<()> {
@@ -344,7 +338,7 @@ impl<'t, I: Interner> Unifier<'t, I> {
 
             (&LifetimeData::Placeholder(_), &LifetimeData::Placeholder(_)) => {
                 if a != b {
-                    Ok(self.push_lifetime_eq_constraint(a.clone(), b.clone()))
+                    Ok(self.push_lifetime_eq_subgoal(a.clone(), b.clone()))
                 } else {
                     Ok(())
                 }
@@ -388,7 +382,7 @@ impl<'t, I: Interner> Unifier<'t, I> {
                 "unify_lifetime_var: {:?} in {:?} cannot see {:?}; pushing constraint",
                 var, var_ui, value_ui
             );
-            Ok(self.push_lifetime_eq_constraint(a.clone(), b.clone()))
+            Ok(self.push_lifetime_eq_subgoal(a.clone(), b.clone()))
         }
     }
 
@@ -478,15 +472,14 @@ impl<'t, I: Interner> Unifier<'t, I> {
         Ok(())
     }
 
-    fn push_lifetime_eq_constraint(&mut self, a: Lifetime<I>, b: Lifetime<I>) {
-        self.constraints.push(InEnvironment::new(
-            self.environment,
-            Constraint::Outlives(a.clone(), b.clone()),
-        ));
-        self.constraints.push(InEnvironment::new(
-            self.environment,
-            Constraint::Outlives(b, a),
-        ));
+    fn push_lifetime_eq_subgoal(&mut self, a: Lifetime<I>, b: Lifetime<I>) {
+        let interner = self.interner;
+        let b_outlives_a = GoalData::AddRegionConstraint(b.clone(), a.clone()).intern(interner);
+        self.goals
+            .push(InEnvironment::new(self.environment, b_outlives_a));
+        let a_outlives_b = GoalData::AddRegionConstraint(a, b).intern(interner);
+        self.goals
+            .push(InEnvironment::new(self.environment, a_outlives_b));
     }
 }
 
@@ -588,10 +581,8 @@ where
             // exists<'x> forall<'b> ?T = Foo<'x>, where 'x = 'b
 
             let tick_x = self.unifier.table.new_variable(self.universe_index);
-            self.unifier.push_lifetime_eq_constraint(
-                tick_x.to_lifetime(interner),
-                ui.to_lifetime(interner),
-            );
+            self.unifier
+                .push_lifetime_eq_subgoal(tick_x.to_lifetime(interner), ui.to_lifetime(interner));
             Ok(tick_x.to_lifetime(interner))
         } else {
             // If the `ui` is higher than `self.universe_index`, then we can name

chalk-solve/src/recursive/fulfill.rs

@@ -99,10 +99,7 @@ pub(super) trait RecursiveInferenceTable<I: Interner> {
         environment: &Environment<I>,
         a: &T,
         b: &T,
-    ) -> Fallible<(
-        Vec<InEnvironment<DomainGoal<I>>>,
-        Vec<InEnvironment<Constraint<I>>>,
-    )>
+    ) -> Fallible<Vec<InEnvironment<Goal<I>>>>
     where
         T: ?Sized + Zip<I>;
 
@@ -259,13 +256,11 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
     where
         T: ?Sized + Zip<I> + Debug,
     {
-        let (goals, constraints) = self
+        let goals = self
             .infer
             .unify(self.solver.interner(), environment, a, b)?;
         debug!("unify({:?}, {:?}) succeeded", a, b);
         debug!("unify: goals={:?}", goals);
-        debug!("unify: constraints={:?}", constraints);
-        self.constraints.extend(constraints);
         for goal in goals {
             let goal = goal.cast(self.solver.interner());
             self.push_obligation(Obligation::Prove(goal));
@@ -309,12 +304,17 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
                 let in_env = InEnvironment::new(environment, subgoal.clone());
                 self.push_obligation(Obligation::Refute(in_env));
             }
+            GoalData::AddRegionConstraint(a, b) => {
+                self.constraints.insert(InEnvironment::new(
+                    &environment,
+                    Constraint::Outlives(a.clone(), b.clone()),
+                ));
+            }
             GoalData::DomainGoal(domain_goal) => match domain_goal {
                 DomainGoal::Holds(WhereClause::LifetimeOutlives(LifetimeOutlives { a, b })) => {
-                    self.constraints.insert(InEnvironment::new(
-                        &environment,
-                        Constraint::Outlives(a.clone(), b.clone()),
-                    ));
+                    let add_constraint =
+                        GoalData::AddRegionConstraint(a.clone(), b.clone()).intern(interner);
+                    self.push_goal(environment, add_constraint)?
                 }
                 _ => {
                     let in_env = InEnvironment::new(environment, goal);

chalk-solve/src/recursive/solve.rs

@@ -10,8 +10,8 @@ use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::visit::Visit;
 use chalk_ir::zip::Zip;
 use chalk_ir::{
-    Binders, Canonical, ClausePriority, Constraint, DomainGoal, Environment, Fallible, Floundered,
-    GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClause, ProgramClauseData,
+    Binders, Canonical, ClausePriority, DomainGoal, Environment, Fallible, Floundered, GenericArg,
+    Goal, GoalData, InEnvironment, NoSolution, ProgramClause, ProgramClauseData,
     ProgramClauseImplication, Substitution, UCanonical, UniverseMap,
 };
 use std::fmt::Debug;
@@ -279,15 +279,12 @@ impl<I: Interner> RecursiveInferenceTable<I> for RecursiveInferenceTableImpl<I>
         environment: &Environment<I>,
         a: &T,
         b: &T,
-    ) -> Fallible<(
-        Vec<InEnvironment<DomainGoal<I>>>,
-        Vec<InEnvironment<Constraint<I>>>,
-    )>
+    ) -> Fallible<Vec<InEnvironment<Goal<I>>>>
     where
         T: ?Sized + Zip<I>,
     {
         let res = self.infer.unify(interner, environment, a, b)?;
-        Ok((res.goals, res.constraints))
+        Ok(res.goals)
     }
 
     fn instantiate_canonical<T>(&mut self, interner: &I, bound: &Canonical<T>) -> T::Result