uniquify root goals during HIR typeck

14 files changed, 180 insertions, 41 deletions

diff --git a/compiler/rustc_hir_typeck/src/typeck_root_ctxt.rs b/compiler/rustc_hir_typeck/src/typeck_root_ctxt.rs
index 9f4ab8ca5d4..20844dee793 100644
--- a/compiler/rustc_hir_typeck/src/typeck_root_ctxt.rs
+++ b/compiler/rustc_hir_typeck/src/typeck_root_ctxt.rs
@@ -85,8 +85,11 @@ impl<'tcx> TypeckRootCtxt<'tcx> {
     pub(crate) fn new(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> Self {
         let hir_owner = tcx.local_def_id_to_hir_id(def_id).owner;
 
-        let infcx =
-            tcx.infer_ctxt().ignoring_regions().build(TypingMode::typeck_for_body(tcx, def_id));
+        let infcx = tcx
+            .infer_ctxt()
+            .ignoring_regions()
+            .in_hir_typeck()
+            .build(TypingMode::typeck_for_body(tcx, def_id));
         let typeck_results = RefCell::new(ty::TypeckResults::new(hir_owner));
         let fulfillment_cx = RefCell::new(<dyn TraitEngine<'_, _>>::new(&infcx));
 
diff --git a/compiler/rustc_infer/src/infer/at.rs b/compiler/rustc_infer/src/infer/at.rs
index 5fe795bd23a..ad19cdef4e7 100644
--- a/compiler/rustc_infer/src/infer/at.rs
+++ b/compiler/rustc_infer/src/infer/at.rs
@@ -71,6 +71,7 @@ impl<'tcx> InferCtxt<'tcx> {
             tcx: self.tcx,
             typing_mode: self.typing_mode,
             considering_regions: self.considering_regions,
+            in_hir_typeck: self.in_hir_typeck,
             skip_leak_check: self.skip_leak_check,
             inner: self.inner.clone(),
             lexical_region_resolutions: self.lexical_region_resolutions.clone(),
@@ -95,6 +96,7 @@ impl<'tcx> InferCtxt<'tcx> {
             tcx: self.tcx,
             typing_mode,
             considering_regions: self.considering_regions,
+            in_hir_typeck: self.in_hir_typeck,
             skip_leak_check: self.skip_leak_check,
             inner: self.inner.clone(),
             lexical_region_resolutions: self.lexical_region_resolutions.clone(),
diff --git a/compiler/rustc_infer/src/infer/context.rs b/compiler/rustc_infer/src/infer/context.rs
index bb9c8850093..21e999b080d 100644
--- a/compiler/rustc_infer/src/infer/context.rs
+++ b/compiler/rustc_infer/src/infer/context.rs
@@ -22,6 +22,10 @@ impl<'tcx> rustc_type_ir::InferCtxtLike for InferCtxt<'tcx> {
         self.next_trait_solver
     }
 
+    fn in_hir_typeck(&self) -> bool {
+        self.in_hir_typeck
+    }
+
     fn typing_mode(&self) -> ty::TypingMode<'tcx> {
         self.typing_mode()
     }
diff --git a/compiler/rustc_infer/src/infer/mod.rs b/compiler/rustc_infer/src/infer/mod.rs
index 2d269e320b6..17c587c5e7f 100644
--- a/compiler/rustc_infer/src/infer/mod.rs
+++ b/compiler/rustc_infer/src/infer/mod.rs
@@ -244,9 +244,28 @@ pub struct InferCtxt<'tcx> {
     typing_mode: TypingMode<'tcx>,
 
     /// Whether this inference context should care about region obligations in
-    /// the root universe. Most notably, this is used during hir typeck as region
+    /// the root universe. Most notably, this is used during HIR typeck as region
     /// solving is left to borrowck instead.
     pub considering_regions: bool,
+    /// Whether this inference context is used by HIR typeck. If so, we uniquify regions
+    /// with `-Znext-solver`. This is necessary as borrowck will start by replacing each
+    /// occurance of a free region with a unique inference variable so if HIR typeck
+    /// ends up depending on two regions being equal we'd get unexpected mismatches
+    /// between HIR typeck and MIR typeck, resulting in an ICE.
+    ///
+    /// The trait solver sometimes depends on regions being identical. As a concrete example
+    /// the trait solver ignores other candidates if one candidate exists without any constraints.
+    /// The goal `&'a u32: Equals<&'a u32>` has no constraints right now, but if we replace
+    /// each occurance of `'a` with a unique region the goal now equates these regions.
+    ///
+    /// See the tests in trait-system-refactor-initiative#27 for concrete examples.
+    ///
+    /// FIXME(-Znext-solver): This is insufficient in theory as a goal `T: Trait<?x, ?x>`
+    /// may rely on the two occurances of `?x` being identical. If `?x` gets inferred to a
+    /// type containing regions, this will no longer be the case. We can handle this case
+    /// by storing goals which hold while still depending on inference vars and then
+    /// reproving them before writeback.
+    pub in_hir_typeck: bool,
 
     /// If set, this flag causes us to skip the 'leak check' during
     /// higher-ranked subtyping operations. This flag is a temporary one used
@@ -506,6 +525,7 @@ pub struct TypeOutlivesConstraint<'tcx> {
 pub struct InferCtxtBuilder<'tcx> {
     tcx: TyCtxt<'tcx>,
     considering_regions: bool,
+    in_hir_typeck: bool,
     skip_leak_check: bool,
     /// Whether we should use the new trait solver in the local inference context,
     /// which affects things like which solver is used in `predicate_may_hold`.
@@ -518,6 +538,7 @@ impl<'tcx> TyCtxt<'tcx> {
         InferCtxtBuilder {
             tcx: self,
             considering_regions: true,
+            in_hir_typeck: false,
             skip_leak_check: false,
             next_trait_solver: self.next_trait_solver_globally(),
         }
@@ -535,6 +556,11 @@ impl<'tcx> InferCtxtBuilder<'tcx> {
         self
     }
 
+    pub fn in_hir_typeck(mut self) -> Self {
+        self.in_hir_typeck = true;
+        self
+    }
+
     pub fn skip_leak_check(mut self, skip_leak_check: bool) -> Self {
         self.skip_leak_check = skip_leak_check;
         self
@@ -568,12 +594,18 @@ impl<'tcx> InferCtxtBuilder<'tcx> {
     }
 
     pub fn build(&mut self, typing_mode: TypingMode<'tcx>) -> InferCtxt<'tcx> {
-        let InferCtxtBuilder { tcx, considering_regions, skip_leak_check, next_trait_solver } =
-            *self;
+        let InferCtxtBuilder {
+            tcx,
+            considering_regions,
+            in_hir_typeck,
+            skip_leak_check,
+            next_trait_solver,
+        } = *self;
         InferCtxt {
             tcx,
             typing_mode,
             considering_regions,
+            in_hir_typeck,
             skip_leak_check,
             inner: RefCell::new(InferCtxtInner::new()),
             lexical_region_resolutions: RefCell::new(None),
diff --git a/compiler/rustc_next_trait_solver/src/canonicalizer.rs b/compiler/rustc_next_trait_solver/src/canonicalizer.rs
index a418aa82100..1bc35e599c7 100644
--- a/compiler/rustc_next_trait_solver/src/canonicalizer.rs
+++ b/compiler/rustc_next_trait_solver/src/canonicalizer.rs
@@ -19,6 +19,20 @@ const NEEDS_CANONICAL: TypeFlags = TypeFlags::from_bits(
 )
 .unwrap();
 
+#[derive(Debug, Clone, Copy)]
+enum CanonicalizeInputKind {
+    /// When canonicalizing the `param_env`, we keep `'static` as merging
+    /// trait candidates relies on it when deciding whether a where-bound
+    /// is trivial.
+    ParamEnv,
+    /// When canonicalizing predicates, we don't keep `'static`. If we're
+    /// currently outside of the trait solver and canonicalize the root goal
+    /// during HIR typeck, we replace each occurance of a region with a
+    /// unique region variable. See the comment on `InferCtxt::in_hir_typeck`
+    /// for more details.
+    Predicate { is_hir_typeck_root_goal: bool },
+}
+
 /// Whether we're canonicalizing a query input or the query response.
 ///
 /// When canonicalizing an input we're in the context of the caller
@@ -26,10 +40,7 @@ const NEEDS_CANONICAL: TypeFlags = TypeFlags::from_bits(
 /// query.
 #[derive(Debug, Clone, Copy)]
 enum CanonicalizeMode {
-    /// When canonicalizing the `param_env`, we keep `'static` as merging
-    /// trait candidates relies on it when deciding whether a where-bound
-    /// is trivial.
-    Input { keep_static: bool },
+    Input(CanonicalizeInputKind),
     /// FIXME: We currently return region constraints referring to
     /// placeholders and inference variables from a binder instantiated
     /// inside of the query.
@@ -122,7 +133,7 @@ impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
                     let mut variables = Vec::new();
                     let mut env_canonicalizer = Canonicalizer {
                         delegate,
-                        canonicalize_mode: CanonicalizeMode::Input { keep_static: true },
+                        canonicalize_mode: CanonicalizeMode::Input(CanonicalizeInputKind::ParamEnv),
 
                         variables: &mut variables,
                         variable_lookup_table: Default::default(),
@@ -154,7 +165,7 @@ impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
         } else {
             let mut env_canonicalizer = Canonicalizer {
                 delegate,
-                canonicalize_mode: CanonicalizeMode::Input { keep_static: true },
+                canonicalize_mode: CanonicalizeMode::Input(CanonicalizeInputKind::ParamEnv),
 
                 variables,
                 variable_lookup_table: Default::default(),
@@ -180,6 +191,7 @@ impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
     pub fn canonicalize_input<P: TypeFoldable<I>>(
         delegate: &'a D,
         variables: &'a mut Vec<I::GenericArg>,
+        is_hir_typeck_root_goal: bool,
         input: QueryInput<I, P>,
     ) -> ty::Canonical<I, QueryInput<I, P>> {
         // First canonicalize the `param_env` while keeping `'static`
@@ -189,7 +201,9 @@ impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
         // while *mostly* reusing the canonicalizer from above.
         let mut rest_canonicalizer = Canonicalizer {
             delegate,
-            canonicalize_mode: CanonicalizeMode::Input { keep_static: false },
+            canonicalize_mode: CanonicalizeMode::Input(CanonicalizeInputKind::Predicate {
+                is_hir_typeck_root_goal,
+            }),
 
             variables,
             variable_lookup_table,
@@ -296,7 +310,7 @@ impl<'a, D: SolverDelegate<Interner = I>, I: Interner> Canonicalizer<'a, D, I> {
         }
     }
 
-    fn cached_fold_ty(&mut self, t: I::Ty) -> I::Ty {
+    fn inner_fold_ty(&mut self, t: I::Ty) -> I::Ty {
         let kind = match t.kind() {
             ty::Infer(i) => match i {
                 ty::TyVar(vid) => {
@@ -413,10 +427,10 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
             // We don't canonicalize `ReStatic` in the `param_env` as we use it
             // when checking whether a `ParamEnv` candidate is global.
             ty::ReStatic => match self.canonicalize_mode {
-                CanonicalizeMode::Input { keep_static: false } => {
+                CanonicalizeMode::Input(CanonicalizeInputKind::Predicate { .. }) => {
                     CanonicalVarKind::Region(ty::UniverseIndex::ROOT)
                 }
-                CanonicalizeMode::Input { keep_static: true }
+                CanonicalizeMode::Input(CanonicalizeInputKind::ParamEnv)
                 | CanonicalizeMode::Response { .. } => return r,
             },
 
@@ -428,12 +442,12 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
             // `ReErased`. We may be able to short-circuit registering region
             // obligations if we encounter a `ReErased` on one side, for example.
             ty::ReErased | ty::ReError(_) => match self.canonicalize_mode {
-                CanonicalizeMode::Input { .. } => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
+                CanonicalizeMode::Input(_) => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
                 CanonicalizeMode::Response { .. } => return r,
             },
 
             ty::ReEarlyParam(_) | ty::ReLateParam(_) => match self.canonicalize_mode {
-                CanonicalizeMode::Input { .. } => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
+                CanonicalizeMode::Input(_) => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
                 CanonicalizeMode::Response { .. } => {
                     panic!("unexpected region in response: {r:?}")
                 }
@@ -441,7 +455,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
 
             ty::RePlaceholder(placeholder) => match self.canonicalize_mode {
                 // We canonicalize placeholder regions as existentials in query inputs.
-                CanonicalizeMode::Input { .. } => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
+                CanonicalizeMode::Input(_) => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
                 CanonicalizeMode::Response { max_input_universe } => {
                     // If we have a placeholder region inside of a query, it must be from
                     // a new universe.
@@ -459,9 +473,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
                     "region vid should have been resolved fully before canonicalization"
                 );
                 match self.canonicalize_mode {
-                    CanonicalizeMode::Input { keep_static: _ } => {
-                        CanonicalVarKind::Region(ty::UniverseIndex::ROOT)
-                    }
+                    CanonicalizeMode::Input(_) => CanonicalVarKind::Region(ty::UniverseIndex::ROOT),
                     CanonicalizeMode::Response { .. } => {
                         CanonicalVarKind::Region(self.delegate.universe_of_lt(vid).unwrap())
                     }
@@ -469,16 +481,34 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
             }
         };
 
-        let var = self.get_or_insert_bound_var(r, kind);
+        let var = if let CanonicalizeMode::Input(CanonicalizeInputKind::Predicate {
+            is_hir_typeck_root_goal: true,
+        }) = self.canonicalize_mode
+        {
+            let var = ty::BoundVar::from(self.variables.len());
+            self.variables.push(r.into());
+            self.var_kinds.push(kind);
+            var
+        } else {
+            self.get_or_insert_bound_var(r, kind)
+        };
 
         Region::new_anon_bound(self.cx(), self.binder_index, var)
     }
 
     fn fold_ty(&mut self, t: I::Ty) -> I::Ty {
-        if let Some(&ty) = self.cache.get(&(self.binder_index, t)) {
+        if let CanonicalizeMode::Input(CanonicalizeInputKind::Predicate {
+            is_hir_typeck_root_goal: true,
+        }) = self.canonicalize_mode
+        {
+            // If we're canonicalizing a root goal during HIR typeck, we
+            // must not use the `cache` as we want to map each occurrence
+            // of a region to a unique existential variable.
+            self.inner_fold_ty(t)
+        } else if let Some(&ty) = self.cache.get(&(self.binder_index, t)) {
             ty
         } else {
-            let res = self.cached_fold_ty(t);
+            let res = self.inner_fold_ty(t);
             let old = self.cache.insert((self.binder_index, t), res);
             assert_eq!(old, None);
             res
@@ -541,9 +571,9 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> TypeFolder<I> for Canonicaliz
 
     fn fold_clauses(&mut self, c: I::Clauses) -> I::Clauses {
         match self.canonicalize_mode {
-            CanonicalizeMode::Input { keep_static: true }
+            CanonicalizeMode::Input(CanonicalizeInputKind::ParamEnv)
             | CanonicalizeMode::Response { max_input_universe: _ } => {}
-            CanonicalizeMode::Input { keep_static: false } => {
+            CanonicalizeMode::Input(CanonicalizeInputKind::Predicate { .. }) => {
                 panic!("erasing 'static in env")
             }
         }
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
index 5ed316aa6b1..de1330ca82a 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/canonical.rs
@@ -55,6 +55,7 @@ where
     /// for each bound variable.
     pub(super) fn canonicalize_goal(
         &self,
+        is_hir_typeck_root_goal: bool,
         goal: Goal<I, I::Predicate>,
     ) -> (Vec<I::GenericArg>, CanonicalInput<I, I::Predicate>) {
         // We only care about one entry per `OpaqueTypeKey` here,
@@ -67,6 +68,7 @@ where
         let canonical = Canonicalizer::canonicalize_input(
             self.delegate,
             &mut orig_values,
+            is_hir_typeck_root_goal,
             QueryInput {
                 goal,
                 predefined_opaques_in_body: self
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
index ce9b794d40d..053ccf285cf 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
@@ -447,7 +447,10 @@ where
             ));
         }
 
-        let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
+        let is_hir_typeck_root_goal = matches!(goal_evaluation_kind, GoalEvaluationKind::Root)
+            && self.delegate.in_hir_typeck();
+
+        let (orig_values, canonical_goal) = self.canonicalize_goal(is_hir_typeck_root_goal, goal);
         let mut goal_evaluation =
             self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
         let canonical_result = self.search_graph.evaluate_goal(
diff --git a/compiler/rustc_next_trait_solver/src/solve/mod.rs b/compiler/rustc_next_trait_solver/src/solve/mod.rs
index 5ea3f0d1061..f39426c7689 100644
--- a/compiler/rustc_next_trait_solver/src/solve/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/mod.rs
@@ -252,8 +252,6 @@ where
             return None;
         }
 
-        // FIXME(-Znext-solver): Add support to merge region constraints in
-        // responses to deal with trait-system-refactor-initiative#27.
         let one = responses[0];
         if responses[1..].iter().all(|&resp| resp == one) {
             return Some(one);
diff --git a/compiler/rustc_type_ir/src/infer_ctxt.rs b/compiler/rustc_type_ir/src/infer_ctxt.rs
index e86a2305e23..b4873c8c71c 100644
--- a/compiler/rustc_type_ir/src/infer_ctxt.rs
+++ b/compiler/rustc_type_ir/src/infer_ctxt.rs
@@ -148,6 +148,10 @@ pub trait InferCtxtLike: Sized {
         true
     }
 
+    fn in_hir_typeck(&self) -> bool {
+        false
+    }
+
     fn typing_mode(&self) -> TypingMode<Self::Interner>;
 
     fn universe(&self) -> ty::UniverseIndex;
diff --git a/tests/crashes/139409.rs b/tests/crashes/139409.rs
deleted file mode 100644
index 68cbfa153de..00000000000
--- a/tests/crashes/139409.rs
+++ /dev/null
@@ -1,12 +0,0 @@
-//@ known-bug: #139409
-//@ compile-flags: -Znext-solver=globally
-
-fn main() {
-    trait B<C> {}
-    impl<C> B<C> for () {}
-    trait D<C, E>: B<C> + B<E> {
-        fn f(&self) {}
-    }
-    impl<C, E> D<C, E> for () {}
-    (&() as &dyn D<&(), &()>).f()
-}
diff --git a/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-1.next.stderr b/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-1.next.stderr
new file mode 100644
index 00000000000..141a07b4be7
--- /dev/null
+++ b/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-1.next.stderr
@@ -0,0 +1,19 @@
+error[E0283]: type annotations needed: cannot satisfy `dyn D<&(), &()>: B<&()>`
+  --> $DIR/ambiguity-due-to-uniquification-1.rs:15:31
+   |
+LL |     (&() as &dyn D<&(), &()>).f()
+   |                               ^
+   |
+   = note: cannot satisfy `dyn D<&(), &()>: B<&()>`
+   = help: the trait `B<C>` is implemented for `()`
+note: required by a bound in `D::f`
+  --> $DIR/ambiguity-due-to-uniquification-1.rs:10:16
+   |
+LL | trait D<C, E>: B<C> + B<E> {
+   |                ^^^^ required by this bound in `D::f`
+LL |     fn f(&self) {}
+   |        - required by a bound in this associated function
+
+error: aborting due to 1 previous error
+
+For more information about this error, try `rustc --explain E0283`.
diff --git a/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-1.rs b/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-1.rs
new file mode 100644
index 00000000000..cfdf74046fb
--- /dev/null
+++ b/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-1.rs
@@ -0,0 +1,17 @@
+//@ revisions: current next
+//@[next] compile-flags: -Znext-solver
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[current] check-pass
+
+// Regression test for #139409 and trait-system-refactor-initiative#27.
+
+trait B<C> {}
+impl<C> B<C> for () {}
+trait D<C, E>: B<C> + B<E> {
+    fn f(&self) {}
+}
+impl<C, E> D<C, E> for () {}
+fn main() {
+    (&() as &dyn D<&(), &()>).f()
+    //[next]~^ ERROR type annotations needed: cannot satisfy `dyn D<&(), &()>: B<&()>`
+}
diff --git a/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-2.next.stderr b/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-2.next.stderr
new file mode 100644
index 00000000000..3b478889996
--- /dev/null
+++ b/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-2.next.stderr
@@ -0,0 +1,17 @@
+error[E0283]: type annotations needed: cannot satisfy `impl Trait<'x> + Trait<'y>: Trait<'y>`
+  --> $DIR/ambiguity-due-to-uniquification-2.rs:16:23
+   |
+LL |     impls_trait::<'y, _>(foo::<'x, 'y>());
+   |                       ^
+   |
+   = note: cannot satisfy `impl Trait<'x> + Trait<'y>: Trait<'y>`
+   = help: the trait `Trait<'t>` is implemented for `()`
+note: required by a bound in `impls_trait`
+  --> $DIR/ambiguity-due-to-uniquification-2.rs:13:23
+   |
+LL | fn impls_trait<'x, T: Trait<'x>>(_: T) {}
+   |                       ^^^^^^^^^ required by this bound in `impls_trait`
+
+error: aborting due to 1 previous error
+
+For more information about this error, try `rustc --explain E0283`.
diff --git a/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-2.rs b/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-2.rs
new file mode 100644
index 00000000000..2a9a8b80cc0
--- /dev/null
+++ b/tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-2.rs
@@ -0,0 +1,20 @@
+//@ revisions: current next
+//@[next] compile-flags: -Znext-solver
+//@ ignore-compare-mode-next-solver (explicit revisions)
+//@[current] check-pass
+
+// Regression test from trait-system-refactor-initiative#27.
+
+trait Trait<'t> {}
+impl<'t> Trait<'t> for () {}
+
+fn foo<'x, 'y>() -> impl Trait<'x> + Trait<'y> {}
+
+fn impls_trait<'x, T: Trait<'x>>(_: T) {}
+
+fn bar<'x, 'y>() {
+    impls_trait::<'y, _>(foo::<'x, 'y>());
+    //[next]~^ ERROR type annotations needed: cannot satisfy `impl Trait<'x> + Trait<'y>: Trait<'y>`
+}
+
+fn main() {}