Rollup merge of #109166 - lcnr:define_opaque_types-explicit, r=oli-obk

make `define_opaque_types` fully explicit

based on the idea of #108389. Moved `define_opaque_types` into the actual operations, e.g. `eq`, instead of `infcx.at` because normalization doesn't use `define_opaque_types` and even creates it's own `At` with a different `define_opaque_types` internally.

Somewhat surprisingly, coherence actually relies on `DefineOpaqueTypes::Yes` for soundness which was revealed because I've incorrectly used `DefineOpaqueTypes::No` in `equate_impl_headers`. It feels concerning that even though this is the case, we still sometimes use `DefineOpaqueTypes::No` in coherence. I did not look into this as part of this PR as it is purely changing the structure of the code without changing behavior in any way.

r? ```@oli-obk```
This commit is contained in:
Matthias Krüger
2023-03-16 08:57:07 +01:00
committed by GitHub
33 changed files with 308 additions and 225 deletions

View File

@@ -17,7 +17,7 @@ use crate::traits::{
use rustc_data_structures::fx::FxIndexSet;
use rustc_errors::Diagnostic;
use rustc_hir::def_id::{DefId, CRATE_DEF_ID, LOCAL_CRATE};
use rustc_infer::infer::{DefiningAnchor, InferCtxt, TyCtxtInferExt};
use rustc_infer::infer::{DefineOpaqueTypes, DefiningAnchor, InferCtxt, TyCtxtInferExt};
use rustc_infer::traits::util;
use rustc_middle::traits::specialization_graph::OverlapMode;
use rustc_middle::ty::fast_reject::{DeepRejectCtxt, TreatParams};
@@ -181,7 +181,7 @@ fn overlap_within_probe<'cx, 'tcx>(
let impl1_header = with_fresh_ty_vars(selcx, param_env, impl1_def_id);
let impl2_header = with_fresh_ty_vars(selcx, param_env, impl2_def_id);
let obligations = equate_impl_headers(selcx, &impl1_header, &impl2_header)?;
let obligations = equate_impl_headers(selcx.infcx, &impl1_header, &impl2_header)?;
debug!("overlap: unification check succeeded");
if overlap_mode.use_implicit_negative() {
@@ -207,20 +207,25 @@ fn overlap_within_probe<'cx, 'tcx>(
Some(OverlapResult { impl_header, intercrate_ambiguity_causes, involves_placeholder })
}
fn equate_impl_headers<'cx, 'tcx>(
selcx: &mut SelectionContext<'cx, 'tcx>,
impl1_header: &ty::ImplHeader<'tcx>,
impl2_header: &ty::ImplHeader<'tcx>,
#[instrument(level = "debug", skip(infcx), ret)]
fn equate_impl_headers<'tcx>(
infcx: &InferCtxt<'tcx>,
impl1: &ty::ImplHeader<'tcx>,
impl2: &ty::ImplHeader<'tcx>,
) -> Option<PredicateObligations<'tcx>> {
// Do `a` and `b` unify? If not, no overlap.
debug!("equate_impl_headers(impl1_header={:?}, impl2_header={:?}", impl1_header, impl2_header);
selcx
.infcx
.at(&ObligationCause::dummy(), ty::ParamEnv::empty())
.define_opaque_types(true)
.eq_impl_headers(impl1_header, impl2_header)
.map(|infer_ok| infer_ok.obligations)
.ok()
let result = match (impl1.trait_ref, impl2.trait_ref) {
(Some(impl1_ref), Some(impl2_ref)) => infcx
.at(&ObligationCause::dummy(), ty::ParamEnv::empty())
.eq(DefineOpaqueTypes::Yes, impl1_ref, impl2_ref),
(None, None) => infcx.at(&ObligationCause::dummy(), ty::ParamEnv::empty()).eq(
DefineOpaqueTypes::Yes,
impl1.self_ty,
impl2.self_ty,
),
_ => bug!("mk_eq_impl_headers given mismatched impl kinds"),
};
result.map(|infer_ok| infer_ok.obligations).ok()
}
/// Given impl1 and impl2 check if both impls can be satisfied by a common type (including
@@ -325,7 +330,7 @@ fn equate<'tcx>(
) -> bool {
// do the impls unify? If not, not disjoint.
let Ok(InferOk { obligations: more_obligations, .. }) =
infcx.at(&ObligationCause::dummy(), impl_env).eq(subject1, subject2)
infcx.at(&ObligationCause::dummy(), impl_env).eq(DefineOpaqueTypes::No,subject1, subject2)
else {
debug!("explicit_disjoint: {:?} does not unify with {:?}", subject1, subject2);
return true;