trait solver: Handle reflexive region constraints

compiler/rustc_type_ir/src/region_constraint.rs

@@ -165,6 +165,13 @@ impl<I: Interner, S: Clone + std::fmt::Debug + Eq + std::hash::Hash> LeafRegionC
 /// An OR of AND of LEAF constraints. Always in "canonical form" meaning:
 /// - No two ANDs are equivalent
 /// - All ANDs are in canonical form
+/// - If any AND is empty, i.e. trivially true, it is the only AND
+///
+/// FIXME(-Zassumptions-on-binders): We should consider a more general canonical form which also
+/// drops any AND that is a superset of another AND. Proving the superset requires strictly more
+/// than proving the subset, so it can never be the candidate which makes the OR hold. E.g.
+/// `OR(AND('a: 'b), AND('a: 'b, 'b: 'c))` really ought to just be `OR(AND('a: 'b))`. Only keeping
+/// an empty AND is the degenerate case of that rule.
 pub struct Or<I: Interner, S: Clone + std::fmt::Debug = ()>(pub Box<[And<I, S>]>);
 impl<I: Interner> Or<I> {
     pub fn with_spans<S: Clone + std::fmt::Debug + Eq + std::hash::Hash>(
@@ -204,6 +211,17 @@ impl<I: Interner, S: Clone + std::hash::Hash + std::fmt::Debug + Eq> Or<I, S> {
         let mut new_ands: Vec<And<I, S>> = Vec::new();
 
         for and in ands {
+            // An empty AND is trivially true, which makes the whole OR true no matter what the
+            // other candidates are. `And::new` discards leaf constraints which are trivially
+            // true, so this is how e.g. a reflexive `'a: 'a` candidate discharges an OR.
+            if and.0.is_empty() {
+                return Self::new_true();
+            }
+
+            // FIXME(-Zassumptions-on-binders): We only discard an AND which is equivalent to one
+            // we already have. More generally we should discard any AND which is a superset of
+            // another, as it requires strictly more to hold. E.g. the second AND in
+            // `OR(AND('a: 'b), AND('a: 'b, 'b: 'c))` is never the one which makes the OR true.
             if new_ands.iter().all(|c| !c.is_and_equivalent_to(&and)) {
                 new_ands.push(and)
             }
@@ -217,7 +235,7 @@ impl<I: Interner, S: Clone + std::hash::Hash + std::fmt::Debug + Eq> Or<I, S> {
     }
 
     pub fn new_leaf(l: LeafRegionConstraint<I, S>) -> Self {
-        Or(Box::new([And(Box::new([l]))]))
+        Or::new([And::new([l])])
     }
 
     pub fn build_and(a: Or<I, S>, b: Or<I, S>) -> Self {
@@ -249,6 +267,7 @@ impl<I: Interner, S: Clone + std::hash::Hash + std::fmt::Debug + Eq> Or<I, S> {
 #[cfg_attr(feature = "nightly", derive(StableHash_NoContext))]
 /// An AND of leaf constraints. Always in "canonical form", meaning:
 /// - No leaf constraints are present twice in this AND
+/// - No leaf constraint is trivially true, i.e. a reflexive `'a: 'a`
 pub struct And<I: Interner, S: Clone + std::fmt::Debug = ()>(pub Box<[LeafRegionConstraint<I, S>]>);
 impl<I: Interner> And<I> {
     pub fn with_spans<S: Clone + std::fmt::Debug + Eq + std::hash::Hash>(
@@ -264,6 +283,15 @@ impl<I: Interner, S: Clone + std::hash::Hash + std::fmt::Debug + Eq> And<I, S> {
         And(i
             .into_iter()
             .filter(|leaf| {
+                // Outlives is reflexive so a `'a: 'a` leaf is always true and carries no
+                // information. Dropping it here keeps the rest of the code from having to special
+                // case it, and is what lets an OR with a reflexive candidate be recognized as true.
+                if let LeafRegionConstraint::RegionOutlives(r1, r2, _) = leaf
+                    && r1 == r2
+                {
+                    return false;
+                }
+
                 if seen.contains(&leaf.clone().without_span()) {
                     false
                 } else {
@@ -409,7 +437,7 @@ impl<I: Interner, S: Clone + std::fmt::Debug + Eq + std::hash::Hash> RegionConst
     }
 
     pub fn new_leaf(l: LeafRegionConstraint<I, S>) -> Self {
-        RegionConstraint { and_constraint: And(Box::new([l])), or_constraint: Or::new_true() }
+        RegionConstraint { and_constraint: And::new([l]), or_constraint: Or::new_true() }
     }
 }
 
@@ -661,6 +689,14 @@ fn pull_region_outlives_constraints_out_of_universe<
                         }
                     };
 
+                    // The constraint may already be entailed by the assumptions of the binder we are
+                    // leaving, e.g. `for<'a, 'b> where 'b: 'a { 'b: 'a }`. There is nothing to lift into
+                    // a smaller universe in that case, and looking for lower universe candidates would
+                    // wrongly result in `Or([])` whenever the placeholders have no lower universe bounds.
+                    if regions_outlived_by(region_1, assumptions).any(|r| r == region_2) {
+                        continue;
+                    }
+
                     let mut candidates = vec![];
 
                     for ub in regions_outlived_by(region_1, assumptions)
@@ -992,7 +1028,6 @@ pub fn regions_outlived_by<I: Interner>(
     r: Region<I>,
     assumptions: &Assumptions<I>,
 ) -> impl Iterator<Item = Region<I>> {
-    // FIXME(-Zassumptions-on-binders): do we need to be adding the reflexive edge here?
     assumptions.region_outlives.reachable_from(r).into_iter().chain([r])
 }
 

tests/ui/assumptions_on_binders/reflexive-outlives-in-root.rs

@@ -0,0 +1,17 @@
+//@ check-pass
+//@ compile-flags: -Zassumptions-on-binders
+
+#![feature(test_binder_constraints, non_lifetime_binders)]
+#![expect(incomplete_features)]
+
+// Root type outlives constraints are destructured into an OR over every region the type is known
+// to outlive. The reflexive `'b: 'b` candidate makes this OR true even though the unrelated
+// `'a: 'b` candidate does not hold. Reflexive leaves are dropped when building an AND, which
+// leaves an empty, i.e. trivially true, AND as one of the candidates of the OR.
+core::test_binder_constraints! {
+    impl<'a, 'b, T: 'a + 'b> {
+        T: 'b
+    }
+}
+
+fn main() {}

tests/ui/assumptions_on_binders/same-universe-placeholder-outlives.rs

@@ -0,0 +1,64 @@
+//@ check-pass
+//@ compile-flags: -Zassumptions-on-binders
+
+#![feature(test_binder_constraints, non_lifetime_binders)]
+#![expect(incomplete_features)]
+
+// Regression test for rust-lang/project-assumptions-on-binders#19.
+//
+// When leaving a binder we lift its region constraints into a smaller universe. Constraints
+// which already hold inside of the binder have no lower universe candidates to be lifted to,
+// so they used to turn into `Or([])`, i.e. `false`. They have to be discharged instead.
+
+// Outlives is reflexive.
+core::test_binder_constraints! {
+    impl<> {
+        forall<'a> {
+            'a: 'a
+        } expect {
+        }
+    }
+}
+
+// Directly entailed by an assumption of the binder we're leaving.
+core::test_binder_constraints! {
+    impl<> {
+        forall<'a, 'b> where 'b: 'a {
+            'b: 'a
+        } expect {
+        }
+    }
+}
+
+// Transitively entailed by the assumptions of the binder we're leaving.
+core::test_binder_constraints! {
+    impl<> {
+        forall<'a, 'b, 'c> where 'c: 'b, 'b: 'a {
+            'c: 'a
+        } expect {
+        }
+    }
+}
+
+// Discharging entailed constraints must not swallow the ones which still have to be lifted
+// into the outer universe. Here `'a: 'a` and `'b: 'a` are discharged inside the binder while
+// `'c: 'a` is lifted, as `'c` outlives every lower universe region that `'a` outlives.
+//
+// FIXME(-Zassumptions-on-binders): this should be `impl<'b, 'c: 'b>`, not
+// `impl<'b, 'c: 'b + 'static>`, but OR isn't actually implemented yet
+core::test_binder_constraints! {
+    impl<'b, 'c: 'b + 'static> {
+        forall<'a> where 'b: 'a {
+            'a: 'a,
+            'b: 'a,
+            'c: 'a,
+        } expect {
+            or {
+                'c: 'b,
+                'c: 'static,
+            }
+        }
+    }
+}
+
+fn main() {}

tests/ui/assumptions_on_binders/test-infra-fails-properly.rs

@@ -60,7 +60,7 @@ core::test_binder_constraints! {
         } expect {
             or {
                 'c: 'b,
-                'c: 'c,
+                'b: 'c,
                 //~^ ERROR forall expect clause failed
             }
         }

tests/ui/assumptions_on_binders/test-infra-fails-properly.stderr

@@ -53,7 +53,7 @@ LL |             T: 'a,
 error: forall expect clause failed
   --> $DIR/test-infra-fails-properly.rs:63:17
    |
-LL |                 'c: 'c,
+LL |                 'b: 'c,
    |                 ^^^^^^
    |
 note: constraint from here
@@ -62,7 +62,7 @@ note: constraint from here
 LL |         forall<'a> where 'b: 'a {
    |         ^^^^^^
    = note: expected: RegionOutlives(
-               'c/#1,
+               'b/#0,
                'c/#1,
                $DIR/test-infra-fails-properly.rs:63:17: 63:23 (#0),
            )