trait_solver: Preserve concrete candidates in ambiguous ORs

compiler/rustc_type_ir/src/region_constraint.rs

@@ -165,6 +165,7 @@ 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
 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 +205,13 @@ 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();
+            }
+
             if new_ands.iter().all(|c| !c.is_and_equivalent_to(&and)) {
                 new_ands.push(and)
             }
@@ -217,7 +225,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 +257,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 +273,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 +427,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() }
     }
 }
 
@@ -576,22 +594,6 @@ pub fn propagate_ambiguity<I: Interner, S: Clone + std::fmt::Debug + Eq + std::h
         return RegionConstraint::new_leaf(ambig.clone());
     }
 
-    for and in constraint.or_constraint.0.iter() {
-        // FIXME(-Zassumptions-on-binders): This is overly conservative. If we have:
-        // `'a: 'b OR ambig` we don't necessarily want to propagate ambiguity here
-        // as we might end up with `'a: 'b` being satisfied in which case we unnecessarily
-        // errored here.
-        //
-        // It's fine if the `ambig` wound up being `false` as that wouldn't cause a goal to
-        // become `NoSolution`, it would instead result in us returning the `'a: 'b` constraint
-        // by itself.
-        //
-        // `rust-lang/project-assumptions-on-binders#21`
-        if let Some(ambig) = and.0.iter().find(|c| c.is_ambig()) {
-            return RegionConstraint::new_leaf(ambig.clone());
-        }
-    }
-
     constraint
 }
 
@@ -661,6 +663,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 +1002,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/mixed-ambiguous-alias-outlives.fail.stderr

@@ -0,0 +1,20 @@
+error: unable to satisfy constraints involving placeholders due to unknown implied bounds
+  --> $DIR/mixed-ambiguous-alias-outlives.rs:35:9
+   |
+LL |         forall<'a, U> {
+   |         ^^^^^^
+
+error: unable to satisfy constraints involving placeholders due to unknown implied bounds
+  --> $DIR/mixed-ambiguous-alias-outlives.rs:63:9
+   |
+LL |         forall<'a, U> {
+   |         ^^^^^^
+
+error: unable to satisfy constraints involving placeholders due to unknown implied bounds
+  --> $DIR/mixed-ambiguous-alias-outlives.rs:75:9
+   |
+LL |         forall<'a, U, V> {
+   |         ^^^^^^
+
+error: aborting due to 3 previous errors
+

tests/ui/assumptions_on_binders/mixed-ambiguous-alias-outlives.rs

@@ -0,0 +1,85 @@
+//@ revisions: pass fail
+//@[pass] check-pass
+//@ compile-flags: -Zassumptions-on-binders
+
+#![feature(test_binder_constraints, non_lifetime_binders)]
+#![expect(incomplete_features)]
+
+trait Project {
+    type Assoc;
+}
+
+impl<T> Project for T {
+    type Assoc = T;
+}
+
+// The alias involving U cannot leave its non-lifetime binder and becomes ambiguous.
+// Keep the other alias candidate until the root, where its outlives assumption is known.
+#[cfg(pass)]
+core::test_binder_constraints! {
+    impl<T: Project<Assoc: 'static>> {
+        forall<'a, U> {
+            or {
+                for<> <U as Project>::Assoc: 'a,
+                for<> T::Assoc: 'a,
+            }
+        }
+    }
+}
+
+// If the concrete candidate is rejected at the root, the ambiguous alternative must
+// still cause an error rather than disappearing with the rejected candidate.
+#[cfg(fail)]
+core::test_binder_constraints! {
+    impl<T: Project> {
+        forall<'a, U> {
+            //[fail]~^ ERROR unable to satisfy constraints involving placeholders
+            or {
+                for<> <U as Project>::Assoc: 'a,
+                for<> T::Assoc: 'a,
+            }
+        }
+    }
+}
+
+// The order of the alternatives must not change whether the bound can be proved.
+#[cfg(pass)]
+core::test_binder_constraints! {
+    impl<T: Project<Assoc: 'static>> {
+        forall<'a, U> {
+            or {
+                for<> T::Assoc: 'a,
+                for<> <U as Project>::Assoc: 'a,
+            }
+        }
+    }
+}
+
+// A required ambiguous constraint still makes the whole AND ambiguous, even when
+// its sibling is known to hold.
+#[cfg(fail)]
+core::test_binder_constraints! {
+    impl<T: Project<Assoc: 'static>> {
+        forall<'a, U> {
+            //[fail]~^ ERROR unable to satisfy constraints involving placeholders
+            for<> <U as Project>::Assoc: 'a,
+            for<> T::Assoc: 'a,
+        }
+    }
+}
+
+// Ambiguity shared by every OR alternative is still required after canonicalization.
+#[cfg(fail)]
+core::test_binder_constraints! {
+    impl {
+        forall<'a, U, V> {
+            //[fail]~^ ERROR unable to satisfy constraints involving placeholders
+            or {
+                for<> <U as Project>::Assoc: 'a,
+                for<> <V as Project>::Assoc: 'a,
+            }
+        }
+    }
+}
+
+fn main() {}

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),
            )