prove super trait bounds when using impls

Author: lcnr

compiler/rustc_next_trait_solver/src/solve/effect_goals.rs

@@ -154,12 +154,27 @@ where
             let impl_trait_ref = impl_trait_ref.instantiate(cx, impl_args);
 
             ecx.eq(goal.param_env, goal.predicate.trait_ref, impl_trait_ref)?;
+            // Resolve inference variables here to improve the debug output :)
+            let impl_trait_ref = ecx.resolve_vars_if_possible(impl_trait_ref);
+
             let where_clause_bounds = cx
                 .predicates_of(impl_def_id)
                 .iter_instantiated(cx, impl_args)
                 .map(|pred| goal.with(cx, pred));
             ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds);
 
+            // When using an impl, we have to check that its super trait bounds are actually satisfied.
+            // This is necessary as otherwise the impl `impl<T: Magic> Magic for T` would allow us to
+            // incorrectly assume all super traits of `Magic`.
+            for clause in elaborate::elaborate(
+                cx,
+                cx.explicit_super_predicates_of(impl_trait_ref.def_id)
+                    .iter_instantiated(cx, impl_trait_ref.args)
+                    .map(|(pred, _)| pred),
+            ) {
+                ecx.add_goal(GoalSource::Misc, goal.with(cx, clause));
+            }
+
             // For this impl to be `const`, we need to check its `~const` bounds too.
             let const_conditions = cx
                 .const_conditions(impl_def_id)

compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs

@@ -228,13 +228,24 @@ where
             let impl_trait_ref = impl_trait_ref.instantiate(cx, impl_args);
 
             ecx.eq(goal.param_env, goal_trait_ref, impl_trait_ref)?;
+            // Resolve inference variables here to improve the debug output :)
+            let impl_trait_ref = ecx.resolve_vars_if_possible(impl_trait_ref);
 
             let where_clause_bounds = cx
                 .predicates_of(impl_def_id)
                 .iter_instantiated(cx, impl_args)
                 .map(|pred| goal.with(cx, pred));
             ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds);
 
+            // Unlike for trait goals, we do not need to check super traits here as they
+            // are only implied for trait clauses. Doing so would result in an unproductive
+            // cycle when normalizing
+            //
+            //     trait Super<T> {}
+            //     trait Trait: Super<Self::Assoc> {
+            //         type Assoc;
+            //     }
+
             // Add GAT where clauses from the trait's definition.
             // FIXME: We don't need these, since these are the type's own WF obligations.
             ecx.add_goals(
@@ -618,7 +629,6 @@ where
                         cx.require_lang_item(TraitSolverLangItem::Sized),
                         [I::GenericArg::from(goal.predicate.self_ty())],
                     );
-                    // FIXME(-Znext-solver=coinductive): Should this be `GoalSource::ImplWhereBound`?
                     ecx.add_goal(GoalSource::Misc, goal.with(cx, sized_predicate));
                     Ty::new_unit(cx)
                 }

compiler/rustc_next_trait_solver/src/solve/trait_goals.rs

@@ -92,23 +92,25 @@ where
             let impl_trait_ref = impl_trait_ref.instantiate(cx, impl_args);
 
             ecx.eq(goal.param_env, goal.predicate.trait_ref, impl_trait_ref)?;
+            // Resolve inference variables here to improve the debug output :)
+            let impl_trait_ref = ecx.resolve_vars_if_possible(impl_trait_ref);
+
             let where_clause_bounds = cx
                 .predicates_of(impl_def_id)
                 .iter_instantiated(cx, impl_args)
                 .map(|pred| goal.with(cx, pred));
             ecx.add_goals(GoalSource::ImplWhereBound, where_clause_bounds);
 
-            // We currently elaborate all supertrait outlives obligations from impls.
-            // This can be removed when we actually do coinduction correctly, and prove
-            // all supertrait obligations unconditionally.
-            let goal_clause: I::Clause = goal.predicate.upcast(cx);
-            for clause in elaborate::elaborate(cx, [goal_clause]) {
-                if matches!(
-                    clause.kind().skip_binder(),
-                    ty::ClauseKind::TypeOutlives(..) | ty::ClauseKind::RegionOutlives(..)
-                ) {
-                    ecx.add_goal(GoalSource::Misc, goal.with(cx, clause));
-                }
+            // When using an impl, we have to check that its super trait bounds are actually satisfied.
+            // This is necessary as otherwise the impl `impl<T: Magic> Magic for T` would allow us to
+            // incorrectly assume all super traits of `Magic`.
+            for clause in elaborate::elaborate(
+                cx,
+                cx.explicit_super_predicates_of(impl_trait_ref.def_id)
+                    .iter_instantiated(cx, impl_trait_ref.args)
+                    .map(|(pred, _)| pred),
+            ) {
+                ecx.add_goal(GoalSource::Misc, goal.with(cx, clause));
             }
 
             ecx.evaluate_added_goals_and_make_canonical_response(maximal_certainty)

compiler/rustc_type_ir/src/solve/mod.rs

@@ -72,8 +72,6 @@ pub enum GoalSource {
     /// changes whether cycles are coinductive.
     ImplWhereBound,
     /// Const conditions that need to hold for `~const` alias bounds to hold.
-    ///
-    /// FIXME(-Znext-solver=coinductive): Are these even coinductive?
     AliasBoundConstCondition,
     /// Instantiating a higher-ranked goal and re-proving it.
     InstantiateHigherRanked,