handle region dependent goals due to infer vars

Author: lcnr

compiler/rustc_hir_typeck/src/lib.rs

@@ -53,7 +53,7 @@ use rustc_hir_analysis::check::{check_abi, check_custom_abi};
 use rustc_hir_analysis::hir_ty_lowering::HirTyLowerer;
 use rustc_infer::traits::{ObligationCauseCode, ObligationInspector, WellFormedLoc};
 use rustc_middle::query::Providers;
-use rustc_middle::ty::{self, Ty, TyCtxt};
+use rustc_middle::ty::{self, Ty, TyCtxt, TypeVisitableExt};
 use rustc_middle::{bug, span_bug};
 use rustc_session::config;
 use rustc_span::Span;
@@ -259,6 +259,21 @@ fn typeck_with_inspect<'tcx>(
 
     let typeck_results = fcx.resolve_type_vars_in_body(body);
 
+    // Handle potentially region dependent goals, see `InferCtxt::in_hir_typeck`.
+    if let None = fcx.infcx.tainted_by_errors() {
+        for obligation in fcx.take_hir_typeck_potentially_region_dependent_goals() {
+            let obligation = fcx.resolve_vars_if_possible(obligation);
+            if obligation.has_non_region_infer() {
+                bug!("unexpected inference variable after writeback: {obligation:?}");
+            }
+            fcx.register_predicate(obligation);
+        }
+        fcx.select_obligations_where_possible(|_| {});
+        if let None = fcx.infcx.tainted_by_errors() {
+            fcx.report_ambiguity_errors();
+        }
+    }
+
     fcx.detect_opaque_types_added_during_writeback();
 
     // Consistency check our TypeckResults instance can hold all ItemLocalIds

compiler/rustc_infer/src/infer/mod.rs

@@ -37,10 +37,11 @@ use snapshot::undo_log::InferCtxtUndoLogs;
 use tracing::{debug, instrument};
 use type_variable::TypeVariableOrigin;
 
-use crate::infer::region_constraints::UndoLog;
+use crate::infer::snapshot::undo_log::UndoLog;
 use crate::infer::unify_key::{ConstVariableOrigin, ConstVariableValue, ConstVidKey};
 use crate::traits::{
-    self, ObligationCause, ObligationInspector, PredicateObligations, TraitEngine,
+    self, ObligationCause, ObligationInspector, PredicateObligation, PredicateObligations,
+    TraitEngine,
 };
 
 pub mod at;
@@ -156,6 +157,12 @@ pub struct InferCtxtInner<'tcx> {
     /// which may cause types to no longer be considered well-formed.
     region_assumptions: Vec<ty::ArgOutlivesPredicate<'tcx>>,
 
+    /// `-Znext-solver`: Successfully proven goals during HIR typeck which
+    /// reference inference variables and get reproven after writeback.
+    ///
+    /// See the documentation of `InferCtxt::in_hir_typeck` for more details.
+    hir_typeck_potentially_region_dependent_goals: Vec<PredicateObligation<'tcx>>,
+
     /// Caches for opaque type inference.
     opaque_type_storage: OpaqueTypeStorage<'tcx>,
 }
@@ -173,6 +180,7 @@ impl<'tcx> InferCtxtInner<'tcx> {
             region_constraint_storage: Some(Default::default()),
             region_obligations: Default::default(),
             region_assumptions: Default::default(),
+            hir_typeck_potentially_region_dependent_goals: Default::default(),
             opaque_type_storage: Default::default(),
         }
     }
@@ -247,24 +255,25 @@ pub struct InferCtxt<'tcx> {
     /// 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.
+    /// `-Znext-solver`: Whether this inference context is used by HIR typeck. If so, we
+    /// need to make sure we don't rely on region identity in the trait solver or for
+    /// type equality. This is necessary as borrowck starts by replacing each occurrence 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.
+    /// 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.
+    /// We handle this by *uniquifying* region when canonicalizing root goals during HIR typeck.
+    /// This is still insufficient as inference variables may *hide* region variables, so e.g.
+    /// `dyn TwoSuper<?x, ?x>: Super<?x>` may hold but MIR typeck could end up having to prove
+    /// `dyn TwoSuper<&'0 (), &'1 ()>: Super<&'2 ()>` which is now ambiguous. Because of this we
+    /// stash all successfully proven goals which reference inference variables and then reprove
+    /// them after writeback.  
     pub in_hir_typeck: bool,
 
     /// If set, this flag causes us to skip the 'leak check' during
@@ -1010,6 +1019,22 @@ impl<'tcx> InferCtxt<'tcx> {
         }
     }
 
+    pub fn push_hir_typeck_potentially_region_dependent_goal(
+        &self,
+        goal: PredicateObligation<'tcx>,
+    ) {
+        let mut inner = self.inner.borrow_mut();
+        inner.undo_log.push(UndoLog::PushHirTypeckPotentiallyRegionDependentGoal);
+        inner.hir_typeck_potentially_region_dependent_goals.push(goal);
+    }
+
+    pub fn take_hir_typeck_potentially_region_dependent_goals(
+        &self,
+    ) -> Vec<PredicateObligation<'tcx>> {
+        assert!(!self.in_snapshot(), "cannot take goals in a snapshot");
+        std::mem::take(&mut self.inner.borrow_mut().hir_typeck_potentially_region_dependent_goals)
+    }
+
     pub fn ty_to_string(&self, t: Ty<'tcx>) -> String {
         self.resolve_vars_if_possible(t).to_string()
     }

compiler/rustc_infer/src/infer/outlives/obligations.rs

@@ -177,6 +177,7 @@ impl<'tcx> InferCtxt<'tcx> {
     }
 
     pub fn take_registered_region_assumptions(&self) -> Vec<ty::ArgOutlivesPredicate<'tcx>> {
+        assert!(!self.in_snapshot(), "cannot take registered region assumptions in a snapshot");
         std::mem::take(&mut self.inner.borrow_mut().region_assumptions)
     }
 

compiler/rustc_infer/src/infer/snapshot/undo_log.rs

@@ -29,6 +29,7 @@ pub(crate) enum UndoLog<'tcx> {
     ProjectionCache(traits::UndoLog<'tcx>),
     PushTypeOutlivesConstraint,
     PushRegionAssumption,
+    PushHirTypeckPotentiallyRegionDependentGoal,
 }
 
 macro_rules! impl_from {
@@ -79,7 +80,12 @@ impl<'tcx> Rollback<UndoLog<'tcx>> for InferCtxtInner<'tcx> {
                 assert_matches!(popped, Some(_), "pushed region constraint but could not pop it");
             }
             UndoLog::PushRegionAssumption => {
-                self.region_assumptions.pop();
+                let popped = self.region_assumptions.pop();
+                assert_matches!(popped, Some(_), "pushed region assumption but could not pop it");
+            }
+            UndoLog::PushHirTypeckPotentiallyRegionDependentGoal => {
+                let popped = self.hir_typeck_potentially_region_dependent_goals.pop();
+                assert_matches!(popped, Some(_), "pushed goal but could not pop it");
             }
         }
     }

compiler/rustc_trait_selection/src/solve/fulfill.rs

@@ -197,7 +197,11 @@ where
                     delegate.compute_goal_fast_path(goal, obligation.cause.span)
                 {
                     match certainty {
-                        Certainty::Yes => {}
+                        Certainty::Yes => {
+                            if infcx.in_hir_typeck && obligation.has_non_region_infer() {
+                                infcx.push_hir_typeck_potentially_region_dependent_goal(obligation);
+                            }
+                        }
                         Certainty::Maybe(_) => {
                             self.obligations.register(obligation, None);
                         }
@@ -230,7 +234,11 @@ where
                 }
 
                 match certainty {
-                    Certainty::Yes => {}
+                    Certainty::Yes => {
+                        if infcx.in_hir_typeck && obligation.has_non_region_infer() {
+                            infcx.push_hir_typeck_potentially_region_dependent_goal(obligation);
+                        }
+                    }
                     Certainty::Maybe(_) => self.obligations.register(obligation, stalled_on),
                 }
             }

tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-3.next.stderr

@@ -0,0 +1,19 @@
+error[E0283]: type annotations needed: cannot satisfy `(dyn Object<&(), &()> + 'static): Trait<&()>`
+  --> $DIR/ambiguity-due-to-uniquification-3.rs:28:17
+   |
+LL |     impls_trait(obj, t);
+   |     ----------- ^^^
+   |     |
+   |     required by a bound introduced by this call
+   |
+   = note: cannot satisfy `(dyn Object<&(), &()> + 'static): Trait<&()>`
+   = help: the trait `Trait<T>` is implemented for `()`
+note: required by a bound in `impls_trait`
+  --> $DIR/ambiguity-due-to-uniquification-3.rs:24:19
+   |
+LL | fn impls_trait<T: Trait<U>, U>(_: Inv<T>, _: Inv<U>) {}
+   |                   ^^^^^^^^ required by this bound in `impls_trait`
+
+error: aborting due to 1 previous error
+
+For more information about this error, try `rustc --explain E0283`.

tests/ui/traits/next-solver/assembly/ambiguity-due-to-uniquification-3.rs

@@ -0,0 +1,33 @@
+//@ 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.
+//
+// Unlike in the previous two tests, `dyn Object<?x, ?y>: Trait<?x>` relies
+// on structural identity of type inference variables. This inference variable
+// gets constrained to a type containing a region later on. To prevent this
+// from causing an ICE during MIR borrowck, we stash goals which depend on
+// inference variables and then reprove them at the end of HIR typeck.
+
+#![feature(rustc_attrs)]
+#![rustc_no_implicit_bounds]
+trait Trait<T> {}
+impl<T> Trait<T> for () {}
+
+trait Object<T, U>: Trait<T> + Trait<U> {}
+
+#[derive(Clone, Copy)]
+struct Inv<T>(*mut T);
+fn foo<T: Sized, U: Sized>() -> (Inv<dyn Object<T, U>>, Inv<T>) { todo!() }
+fn impls_trait<T: Trait<U>, U>(_: Inv<T>, _: Inv<U>) {}
+
+fn bar() {
+    let (obj, t) = foo();
+    impls_trait(obj, t);
+    //[next]~^ ERROR type annotations needed
+    let _: Inv<dyn Object<&(), &()>> = obj;
+}
+
+fn main() {}