From f518827503f8a88e3ecad9a7645d4fc7cd8cfebe Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Fri, 21 Jan 2022 10:50:42 -0300
Subject: [PATCH 01/12] Use impl1 and impl2 instead of a and b prefixes

---
 .../src/traits/coherence.rs                   | 32 +++++++++----------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index af3540386f9fc..a875e2ccf950f 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -140,21 +140,21 @@ fn with_fresh_ty_vars<'cx, 'tcx>(
 fn overlap<'cx, 'tcx>(
     selcx: &mut SelectionContext<'cx, 'tcx>,
     skip_leak_check: SkipLeakCheck,
-    a_def_id: DefId,
-    b_def_id: DefId,
+    impl1_def_id: DefId,
+    impl2_def_id: DefId,
 ) -> Option<OverlapResult<'tcx>> {
-    debug!("overlap(a_def_id={:?}, b_def_id={:?})", a_def_id, b_def_id);
+    debug!("overlap(impl1_def_id={:?}, impl2_def_id={:?})", impl1_def_id, impl2_def_id);
 
     selcx.infcx().probe_maybe_skip_leak_check(skip_leak_check.is_yes(), |snapshot| {
-        overlap_within_probe(selcx, skip_leak_check, a_def_id, b_def_id, snapshot)
+        overlap_within_probe(selcx, skip_leak_check, impl1_def_id, impl2_def_id, snapshot)
     })
 }
 
 fn overlap_within_probe<'cx, 'tcx>(
     selcx: &mut SelectionContext<'cx, 'tcx>,
     skip_leak_check: SkipLeakCheck,
-    a_def_id: DefId,
-    b_def_id: DefId,
+    impl1_def_id: DefId,
+    impl2_def_id: DefId,
     snapshot: &CombinedSnapshot<'_, 'tcx>,
 ) -> Option<OverlapResult<'tcx>> {
     fn loose_check<'cx, 'tcx>(
@@ -182,17 +182,17 @@ fn overlap_within_probe<'cx, 'tcx>(
     // empty environment.
     let param_env = ty::ParamEnv::empty();
 
-    let a_impl_header = with_fresh_ty_vars(selcx, param_env, a_def_id);
-    let b_impl_header = with_fresh_ty_vars(selcx, param_env, b_def_id);
+    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);
 
-    debug!("overlap: a_impl_header={:?}", a_impl_header);
-    debug!("overlap: b_impl_header={:?}", b_impl_header);
+    debug!("overlap: impl1_header={:?}", impl1_header);
+    debug!("overlap: impl2_header={:?}", impl2_header);
 
     // Do `a` and `b` unify? If not, no overlap.
     let obligations = match selcx
         .infcx()
         .at(&ObligationCause::dummy(), param_env)
-        .eq_impl_headers(&a_impl_header, &b_impl_header)
+        .eq_impl_headers(&impl1_header, &impl2_header)
     {
         Ok(InferOk { obligations, value: () }) => obligations,
         Err(_) => {
@@ -225,11 +225,11 @@ fn overlap_within_probe<'cx, 'tcx>(
     // at some point an impl for `&'?a str: Error` could be added.
     let infcx = selcx.infcx();
     let tcx = infcx.tcx;
-    let opt_failing_obligation = a_impl_header
+    let opt_failing_obligation = impl1_header
         .predicates
         .iter()
         .copied()
-        .chain(b_impl_header.predicates)
+        .chain(impl2_header.predicates)
         .map(|p| infcx.resolve_vars_if_possible(p))
         .map(|p| Obligation {
             cause: ObligationCause::dummy(),
@@ -241,8 +241,8 @@ fn overlap_within_probe<'cx, 'tcx>(
         .find(|o| {
             // if both impl headers are set to strict coherence it means that this will be accepted
             // only if it's stated that T: !Trait. So only prove that the negated obligation holds.
-            if tcx.has_attr(a_def_id, sym::rustc_strict_coherence)
-                && tcx.has_attr(b_def_id, sym::rustc_strict_coherence)
+            if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence)
+                && tcx.has_attr(impl2_def_id, sym::rustc_strict_coherence)
             {
                 strict_check(selcx, o)
             } else {
@@ -265,7 +265,7 @@ fn overlap_within_probe<'cx, 'tcx>(
         }
     }
 
-    let impl_header = selcx.infcx().resolve_vars_if_possible(a_impl_header);
+    let impl_header = selcx.infcx().resolve_vars_if_possible(impl1_header);
     let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
     debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);
 

From 052b31b5874a509a642a28cae0e20fe6031e766a Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Fri, 21 Jan 2022 10:53:17 -0300
Subject: [PATCH 02/12] Move auxiliary fns out of overlap_with_probe

---
 .../src/traits/coherence.rs                   | 38 +++++++++----------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index a875e2ccf950f..4383836b98bb9 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -157,25 +157,6 @@ fn overlap_within_probe<'cx, 'tcx>(
     impl2_def_id: DefId,
     snapshot: &CombinedSnapshot<'_, 'tcx>,
 ) -> Option<OverlapResult<'tcx>> {
-    fn loose_check<'cx, 'tcx>(
-        selcx: &mut SelectionContext<'cx, 'tcx>,
-        o: &PredicateObligation<'tcx>,
-    ) -> bool {
-        !selcx.predicate_may_hold_fatal(o)
-    }
-
-    fn strict_check<'cx, 'tcx>(
-        selcx: &SelectionContext<'cx, 'tcx>,
-        o: &PredicateObligation<'tcx>,
-    ) -> bool {
-        let infcx = selcx.infcx();
-        let tcx = infcx.tcx;
-        o.flip_polarity(tcx)
-            .as_ref()
-            .map(|o| selcx.infcx().predicate_must_hold_modulo_regions(o))
-            .unwrap_or(false)
-    }
-
     // For the purposes of this check, we don't bring any placeholder
     // types into scope; instead, we replace the generic types with
     // fresh type variables, and hence we do our evaluations in an
@@ -275,6 +256,25 @@ fn overlap_within_probe<'cx, 'tcx>(
     Some(OverlapResult { impl_header, intercrate_ambiguity_causes, involves_placeholder })
 }
 
+fn loose_check<'cx, 'tcx>(
+    selcx: &mut SelectionContext<'cx, 'tcx>,
+    o: &PredicateObligation<'tcx>,
+) -> bool {
+    !selcx.predicate_may_hold_fatal(o)
+}
+
+fn strict_check<'cx, 'tcx>(
+    selcx: &SelectionContext<'cx, 'tcx>,
+    o: &PredicateObligation<'tcx>,
+) -> bool {
+    let infcx = selcx.infcx();
+    let tcx = infcx.tcx;
+    o.flip_polarity(tcx)
+        .as_ref()
+        .map(|o| selcx.infcx().predicate_must_hold_modulo_regions(o))
+        .unwrap_or(false)
+}
+
 pub fn trait_ref_is_knowable<'tcx>(
     tcx: TyCtxt<'tcx>,
     trait_ref: ty::TraitRef<'tcx>,

From b2a45f064514e06908564153014f8860b8b206d2 Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Fri, 21 Jan 2022 11:02:52 -0300
Subject: [PATCH 03/12] Extract stable_disjoint fn

---
 .../src/traits/coherence.rs                   | 62 ++++++++++++-------
 1 file changed, 41 insertions(+), 21 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index 4383836b98bb9..84b934c19f9d3 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -157,6 +157,9 @@ fn overlap_within_probe<'cx, 'tcx>(
     impl2_def_id: DefId,
     snapshot: &CombinedSnapshot<'_, 'tcx>,
 ) -> Option<OverlapResult<'tcx>> {
+    let infcx = selcx.infcx();
+    let tcx = infcx.tcx;
+
     // For the purposes of this check, we don't bring any placeholder
     // types into scope; instead, we replace the generic types with
     // fresh type variables, and hence we do our evaluations in an
@@ -166,6 +169,39 @@ 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 strict_coherence = tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence)
+        && tcx.has_attr(impl2_def_id, sym::rustc_strict_coherence);
+
+    if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, strict_coherence) {
+        return None;
+    }
+
+    if !skip_leak_check.is_yes() {
+        if infcx.leak_check(true, snapshot).is_err() {
+            debug!("overlap: leak check failed");
+            return None;
+        }
+    }
+
+    let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
+    debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);
+
+    let involves_placeholder =
+        matches!(selcx.infcx().region_constraints_added_in_snapshot(snapshot), Some(true));
+
+    let impl_header = selcx.infcx().resolve_vars_if_possible(impl1_header);
+    Some(OverlapResult { impl_header, intercrate_ambiguity_causes, involves_placeholder })
+}
+
+/// Given impl1 and impl2 check if both impls can be satisfied by a common type (including
+/// where-clauses) If so, return false, otherwise return true, they are disjoint.
+fn stable_disjoint<'cx, 'tcx>(
+    selcx: &mut SelectionContext<'cx, 'tcx>,
+    param_env: ty::ParamEnv<'tcx>,
+    impl1_header: &ty::ImplHeader<'tcx>,
+    impl2_header: ty::ImplHeader<'tcx>,
+    strict_coherence: bool,
+) -> bool {
     debug!("overlap: impl1_header={:?}", impl1_header);
     debug!("overlap: impl2_header={:?}", impl2_header);
 
@@ -177,7 +213,7 @@ fn overlap_within_probe<'cx, 'tcx>(
     {
         Ok(InferOk { obligations, value: () }) => obligations,
         Err(_) => {
-            return None;
+            return true;
         }
     };
 
@@ -222,9 +258,7 @@ fn overlap_within_probe<'cx, 'tcx>(
         .find(|o| {
             // if both impl headers are set to strict coherence it means that this will be accepted
             // only if it's stated that T: !Trait. So only prove that the negated obligation holds.
-            if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence)
-                && tcx.has_attr(impl2_def_id, sym::rustc_strict_coherence)
-            {
+            if strict_coherence {
                 strict_check(selcx, o)
             } else {
                 loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
@@ -236,24 +270,10 @@ fn overlap_within_probe<'cx, 'tcx>(
 
     if let Some(failing_obligation) = opt_failing_obligation {
         debug!("overlap: obligation unsatisfiable {:?}", failing_obligation);
-        return None;
-    }
-
-    if !skip_leak_check.is_yes() {
-        if infcx.leak_check(true, snapshot).is_err() {
-            debug!("overlap: leak check failed");
-            return None;
-        }
+        true
+    } else {
+        false
     }
-
-    let impl_header = selcx.infcx().resolve_vars_if_possible(impl1_header);
-    let intercrate_ambiguity_causes = selcx.take_intercrate_ambiguity_causes();
-    debug!("overlap: intercrate_ambiguity_causes={:#?}", intercrate_ambiguity_causes);
-
-    let involves_placeholder =
-        matches!(selcx.infcx().region_constraints_added_in_snapshot(snapshot), Some(true));
-
-    Some(OverlapResult { impl_header, intercrate_ambiguity_causes, involves_placeholder })
 }
 
 fn loose_check<'cx, 'tcx>(

From c2890ed426aaef4b680848e793a2a741e517a6cc Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Fri, 21 Jan 2022 12:22:13 -0300
Subject: [PATCH 04/12] Add overlap mode

---
 .../src/traits/coherence.rs                   | 36 ++++++++++++++-----
 1 file changed, 27 insertions(+), 9 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index 84b934c19f9d3..170740d2cbdc1 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -135,6 +135,25 @@ fn with_fresh_ty_vars<'cx, 'tcx>(
     header
 }
 
+enum OverlapMode {
+    Stable,
+    Strict,
+}
+
+fn overlap_mode<'tcx>(tcx: TyCtxt<'tcx>, impl1_def_id: DefId, impl2_def_id: DefId) -> OverlapMode {
+    if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence)
+        != tcx.has_attr(impl2_def_id, sym::rustc_strict_coherence)
+    {
+        bug!("Use strict coherence on both impls",);
+    }
+
+    if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence) {
+        OverlapMode::Strict
+    } else {
+        OverlapMode::Stable
+    }
+}
+
 /// Can both impl `a` and impl `b` be satisfied by a common type (including
 /// where-clauses)? If so, returns an `ImplHeader` that unifies the two impls.
 fn overlap<'cx, 'tcx>(
@@ -169,10 +188,8 @@ 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 strict_coherence = tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence)
-        && tcx.has_attr(impl2_def_id, sym::rustc_strict_coherence);
-
-    if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, strict_coherence) {
+    let overlap_mode = overlap_mode(tcx, impl1_def_id, impl2_def_id);
+    if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, overlap_mode) {
         return None;
     }
 
@@ -200,7 +217,7 @@ fn stable_disjoint<'cx, 'tcx>(
     param_env: ty::ParamEnv<'tcx>,
     impl1_header: &ty::ImplHeader<'tcx>,
     impl2_header: ty::ImplHeader<'tcx>,
-    strict_coherence: bool,
+    overlap_mode: OverlapMode,
 ) -> bool {
     debug!("overlap: impl1_header={:?}", impl1_header);
     debug!("overlap: impl2_header={:?}", impl2_header);
@@ -258,10 +275,11 @@ fn stable_disjoint<'cx, 'tcx>(
         .find(|o| {
             // if both impl headers are set to strict coherence it means that this will be accepted
             // only if it's stated that T: !Trait. So only prove that the negated obligation holds.
-            if strict_coherence {
-                strict_check(selcx, o)
-            } else {
-                loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
+            match overlap_mode {
+                OverlapMode::Stable => {
+                    loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
+                }
+                OverlapMode::Strict => strict_check(selcx, o),
             }
         });
     // FIXME: the call to `selcx.predicate_may_hold_fatal` above should be ported

From d2d25a5be0c45b8aa247a3d0b6c7fda12e9ede9a Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Fri, 21 Jan 2022 12:53:50 -0300
Subject: [PATCH 05/12] Implement stable with negative coherence mode

---
 compiler/rustc_feature/src/builtin_attrs.rs   |  1 +
 compiler/rustc_span/src/symbol.rs             |  1 +
 .../src/traits/coherence.rs                   | 99 ++++++++++++++++++-
 .../ui/coherence/auxiliary/option_future.rs   |  8 ++
 .../coherence-overlap-negative-trait2.rs      | 18 ++++
 5 files changed, 123 insertions(+), 4 deletions(-)
 create mode 100644 src/test/ui/coherence/auxiliary/option_future.rs
 create mode 100644 src/test/ui/coherence/coherence-overlap-negative-trait2.rs

diff --git a/compiler/rustc_feature/src/builtin_attrs.rs b/compiler/rustc_feature/src/builtin_attrs.rs
index 723cc06864a90..0e643ff599834 100644
--- a/compiler/rustc_feature/src/builtin_attrs.rs
+++ b/compiler/rustc_feature/src/builtin_attrs.rs
@@ -697,6 +697,7 @@ pub const BUILTIN_ATTRIBUTES: &[BuiltinAttribute] = &[
     rustc_attr!(TEST, rustc_capture_analysis, Normal, template!(Word), WarnFollowing),
     rustc_attr!(TEST, rustc_insignificant_dtor, Normal, template!(Word), WarnFollowing),
     rustc_attr!(TEST, rustc_strict_coherence, Normal, template!(Word), WarnFollowing),
+    rustc_attr!(TEST, rustc_with_negative_coherence, Normal, template!(Word), WarnFollowing),
     rustc_attr!(TEST, rustc_variance, Normal, template!(Word), WarnFollowing),
     rustc_attr!(TEST, rustc_layout, Normal, template!(List: "field1, field2, ..."), WarnFollowing),
     rustc_attr!(TEST, rustc_regions, Normal, template!(Word), WarnFollowing),
diff --git a/compiler/rustc_span/src/symbol.rs b/compiler/rustc_span/src/symbol.rs
index 702e359466079..7e0ce89be67fc 100644
--- a/compiler/rustc_span/src/symbol.rs
+++ b/compiler/rustc_span/src/symbol.rs
@@ -1203,6 +1203,7 @@ symbols! {
         rustc_trivial_field_reads,
         rustc_unsafe_specialization_marker,
         rustc_variance,
+        rustc_with_negative_coherence,
         rustdoc,
         rustdoc_internals,
         rustfmt,
diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index 170740d2cbdc1..42b7139c00698 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -7,9 +7,11 @@
 use crate::infer::{CombinedSnapshot, InferOk, TyCtxtInferExt};
 use crate::traits::query::evaluate_obligation::InferCtxtExt;
 use crate::traits::select::IntercrateAmbiguityCause;
+use crate::traits::util::impl_trait_ref_and_oblig;
 use crate::traits::SkipLeakCheck;
 use crate::traits::{
-    self, Normalized, Obligation, ObligationCause, PredicateObligation, SelectionContext,
+    self, FulfillmentContext, Normalized, Obligation, ObligationCause, PredicateObligation,
+    SelectionContext,
 };
 use rustc_hir::def_id::{DefId, LOCAL_CRATE};
 use rustc_middle::ty::fast_reject::{self, SimplifyParams, StripReferences};
@@ -137,6 +139,7 @@ fn with_fresh_ty_vars<'cx, 'tcx>(
 
 enum OverlapMode {
     Stable,
+    WithNegative,
     Strict,
 }
 
@@ -147,8 +150,16 @@ fn overlap_mode<'tcx>(tcx: TyCtxt<'tcx>, impl1_def_id: DefId, impl2_def_id: DefI
         bug!("Use strict coherence on both impls",);
     }
 
+    if tcx.has_attr(impl1_def_id, sym::rustc_with_negative_coherence)
+        != tcx.has_attr(impl2_def_id, sym::rustc_with_negative_coherence)
+    {
+        bug!("Use with negative coherence on both impls",);
+    }
+
     if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence) {
         OverlapMode::Strict
+    } else if tcx.has_attr(impl1_def_id, sym::rustc_with_negative_coherence) {
+        OverlapMode::WithNegative
     } else {
         OverlapMode::Stable
     }
@@ -188,9 +199,25 @@ 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 overlap_mode = overlap_mode(tcx, impl1_def_id, impl2_def_id);
-    if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, overlap_mode) {
-        return None;
+    match overlap_mode(tcx, impl1_def_id, impl2_def_id) {
+        OverlapMode::Stable => {
+            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, OverlapMode::Stable) {
+                return None;
+            }
+        }
+        OverlapMode::Strict => {
+            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, OverlapMode::Strict) {
+                return None;
+            }
+        }
+        OverlapMode::WithNegative => {
+            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, OverlapMode::Stable)
+                || explicit_disjoint(selcx, impl1_def_id, impl2_def_id)
+                || explicit_disjoint(selcx, impl2_def_id, impl1_def_id)
+            {
+                return None;
+            }
+        }
     }
 
     if !skip_leak_check.is_yes() {
@@ -280,6 +307,7 @@ fn stable_disjoint<'cx, 'tcx>(
                     loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
                 }
                 OverlapMode::Strict => strict_check(selcx, o),
+                OverlapMode::WithNegative => loose_check(selcx, o),
             }
         });
     // FIXME: the call to `selcx.predicate_may_hold_fatal` above should be ported
@@ -294,6 +322,69 @@ fn stable_disjoint<'cx, 'tcx>(
     }
 }
 
+/// Given impl1 and impl2 check if both impls are never satisfied by a common type (including
+/// where-clauses) If so, return true, they are disjoint and false otherwise.
+fn explicit_disjoint<'cx, 'tcx>(
+    selcx: &mut SelectionContext<'cx, 'tcx>,
+    impl1_def_id: DefId,
+    impl2_def_id: DefId,
+) -> bool {
+    let tcx = selcx.infcx().tcx;
+
+    // create a parameter environment corresponding to a (placeholder) instantiation of impl1
+    let impl1_env = tcx.param_env(impl1_def_id);
+    let impl1_trait_ref = tcx.impl_trait_ref(impl1_def_id).unwrap();
+
+    // Create an infcx, taking the predicates of impl1 as assumptions:
+    tcx.infer_ctxt().enter(|infcx| {
+        // Normalize the trait reference. The WF rules ought to ensure
+        // that this always succeeds.
+        let impl1_trait_ref = match traits::fully_normalize(
+            &infcx,
+            FulfillmentContext::new(),
+            ObligationCause::dummy(),
+            impl1_env,
+            impl1_trait_ref,
+        ) {
+            Ok(impl1_trait_ref) => impl1_trait_ref,
+            Err(err) => {
+                bug!("failed to fully normalize {:?}: {:?}", impl1_trait_ref, err);
+            }
+        };
+
+        // Attempt to prove that impl2 applies, given all of the above.
+        let selcx = &mut SelectionContext::new(&infcx);
+        let impl2_substs = infcx.fresh_substs_for_item(DUMMY_SP, impl2_def_id);
+        let (impl2_trait_ref, obligations) =
+            impl_trait_ref_and_oblig(selcx, impl1_env, impl2_def_id, impl2_substs);
+
+        // do the impls unify? If not, not disjoint.
+        let more_obligations = match infcx
+            .at(&ObligationCause::dummy(), impl1_env)
+            .eq(impl1_trait_ref, impl2_trait_ref)
+        {
+            Ok(InferOk { obligations, .. }) => obligations,
+            Err(_) => {
+                debug!(
+                    "explicit_disjoint: {:?} does not unify with {:?}",
+                    impl1_trait_ref, impl2_trait_ref
+                );
+                return false;
+            }
+        };
+
+        let opt_failing_obligation =
+            obligations.into_iter().chain(more_obligations).find(|o| strict_check(selcx, o));
+
+        if let Some(failing_obligation) = opt_failing_obligation {
+            debug!("overlap: obligation unsatisfiable {:?}", failing_obligation);
+            true
+        } else {
+            false
+        }
+    })
+}
+
 fn loose_check<'cx, 'tcx>(
     selcx: &mut SelectionContext<'cx, 'tcx>,
     o: &PredicateObligation<'tcx>,
diff --git a/src/test/ui/coherence/auxiliary/option_future.rs b/src/test/ui/coherence/auxiliary/option_future.rs
new file mode 100644
index 0000000000000..f71df1b87fcda
--- /dev/null
+++ b/src/test/ui/coherence/auxiliary/option_future.rs
@@ -0,0 +1,8 @@
+#![crate_type = "lib"]
+#![feature(negative_impls)]
+#![feature(rustc_attrs)]
+
+pub trait Future {}
+
+#[rustc_with_negative_coherence]
+impl<E> !Future for Option<E> where E: Sized {}
diff --git a/src/test/ui/coherence/coherence-overlap-negative-trait2.rs b/src/test/ui/coherence/coherence-overlap-negative-trait2.rs
new file mode 100644
index 0000000000000..1f47b5ba46e41
--- /dev/null
+++ b/src/test/ui/coherence/coherence-overlap-negative-trait2.rs
@@ -0,0 +1,18 @@
+// check-pass
+// aux-build:option_future.rs
+//
+// Check that if we promise to not impl what would overlap it doesn't actually overlap
+
+#![feature(rustc_attrs)]
+
+extern crate option_future as lib;
+use lib::Future;
+
+trait Termination {}
+
+#[rustc_with_negative_coherence]
+impl<E> Termination for Option<E> where E: Sized {}
+#[rustc_with_negative_coherence]
+impl<F> Termination for F where F: Future + Sized {}
+
+fn main() {}

From 1ec962fb349f0d4a010af81e7ae0d53fec4e2bb2 Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Fri, 21 Jan 2022 15:16:42 -0300
Subject: [PATCH 06/12] Do not pass OverlapMode down, just create a closure to
 properly set the filtering

---
 .../src/traits/coherence.rs                   | 49 +++++++++++++------
 1 file changed, 33 insertions(+), 16 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index 42b7139c00698..f6101d78f4139 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -201,17 +201,17 @@ fn overlap_within_probe<'cx, 'tcx>(
 
     match overlap_mode(tcx, impl1_def_id, impl2_def_id) {
         OverlapMode::Stable => {
-            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, OverlapMode::Stable) {
+            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header) {
                 return None;
             }
         }
         OverlapMode::Strict => {
-            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, OverlapMode::Strict) {
+            if strict_disjoint(selcx, param_env, &impl1_header, impl2_header) {
                 return None;
             }
         }
         OverlapMode::WithNegative => {
-            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header, OverlapMode::Stable)
+            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header)
                 || explicit_disjoint(selcx, impl1_def_id, impl2_def_id)
                 || explicit_disjoint(selcx, impl2_def_id, impl1_def_id)
             {
@@ -244,7 +244,35 @@ fn stable_disjoint<'cx, 'tcx>(
     param_env: ty::ParamEnv<'tcx>,
     impl1_header: &ty::ImplHeader<'tcx>,
     impl2_header: ty::ImplHeader<'tcx>,
-    overlap_mode: OverlapMode,
+) -> bool {
+    let infcx = selcx.infcx();
+    let tcx = infcx.tcx;
+
+    disjoint_with_filter(selcx, param_env, impl1_header, impl2_header, |selcx, o| {
+        loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
+    })
+}
+
+fn strict_disjoint<'cx, 'tcx>(
+    selcx: &mut SelectionContext<'cx, 'tcx>,
+    param_env: ty::ParamEnv<'tcx>,
+    impl1_header: &ty::ImplHeader<'tcx>,
+    impl2_header: ty::ImplHeader<'tcx>,
+) -> bool {
+    disjoint_with_filter(selcx, param_env, impl1_header, impl2_header, |selcx, o| {
+        strict_check(selcx, o)
+    })
+}
+
+fn disjoint_with_filter<'cx, 'tcx>(
+    selcx: &mut SelectionContext<'cx, 'tcx>,
+    param_env: ty::ParamEnv<'tcx>,
+    impl1_header: &ty::ImplHeader<'tcx>,
+    impl2_header: ty::ImplHeader<'tcx>,
+    mut filter: impl FnMut(
+        &mut SelectionContext<'cx, 'tcx>,
+        &rustc_infer::traits::Obligation<'tcx, rustc_middle::ty::Predicate<'tcx>>,
+    ) -> bool,
 ) -> bool {
     debug!("overlap: impl1_header={:?}", impl1_header);
     debug!("overlap: impl2_header={:?}", impl2_header);
@@ -285,7 +313,6 @@ fn stable_disjoint<'cx, 'tcx>(
     // hold we need to check if `&'?a str: !Error` holds, if doesn't hold there's overlap because
     // at some point an impl for `&'?a str: Error` could be added.
     let infcx = selcx.infcx();
-    let tcx = infcx.tcx;
     let opt_failing_obligation = impl1_header
         .predicates
         .iter()
@@ -299,17 +326,7 @@ fn stable_disjoint<'cx, 'tcx>(
             predicate: p,
         })
         .chain(obligations)
-        .find(|o| {
-            // if both impl headers are set to strict coherence it means that this will be accepted
-            // only if it's stated that T: !Trait. So only prove that the negated obligation holds.
-            match overlap_mode {
-                OverlapMode::Stable => {
-                    loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
-                }
-                OverlapMode::Strict => strict_check(selcx, o),
-                OverlapMode::WithNegative => loose_check(selcx, o),
-            }
-        });
+        .find(|o| filter(selcx, o));
     // FIXME: the call to `selcx.predicate_may_hold_fatal` above should be ported
     // to the canonical trait query form, `infcx.predicate_may_hold`, once
     // the new system supports intercrate mode (which coherence needs).

From 19e3c860037a8bb01157aa9da291003c8b69e18c Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Fri, 21 Jan 2022 15:26:05 -0300
Subject: [PATCH 07/12] Make strict_disjoint use explicit_disjoint

---
 .../src/traits/coherence.rs                   | 21 +++++++++++--------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index f6101d78f4139..178cff9501d73 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -206,14 +206,19 @@ fn overlap_within_probe<'cx, 'tcx>(
             }
         }
         OverlapMode::Strict => {
-            if strict_disjoint(selcx, param_env, &impl1_header, impl2_header) {
+            if strict_disjoint(selcx, impl1_def_id, impl2_def_id) {
                 return None;
             }
+
+            // Equate for error reporting
+            let _ = selcx
+                .infcx()
+                .at(&ObligationCause::dummy(), param_env)
+                .eq_impl_headers(&impl1_header, &impl2_header);
         }
         OverlapMode::WithNegative => {
             if stable_disjoint(selcx, param_env, &impl1_header, impl2_header)
-                || explicit_disjoint(selcx, impl1_def_id, impl2_def_id)
-                || explicit_disjoint(selcx, impl2_def_id, impl1_def_id)
+                || strict_disjoint(selcx, impl1_def_id, impl2_def_id)
             {
                 return None;
             }
@@ -255,13 +260,11 @@ fn stable_disjoint<'cx, 'tcx>(
 
 fn strict_disjoint<'cx, 'tcx>(
     selcx: &mut SelectionContext<'cx, 'tcx>,
-    param_env: ty::ParamEnv<'tcx>,
-    impl1_header: &ty::ImplHeader<'tcx>,
-    impl2_header: ty::ImplHeader<'tcx>,
+    impl1_def_id: DefId,
+    impl2_def_id: DefId,
 ) -> bool {
-    disjoint_with_filter(selcx, param_env, impl1_header, impl2_header, |selcx, o| {
-        strict_check(selcx, o)
-    })
+    explicit_disjoint(selcx, impl1_def_id, impl2_def_id)
+        || explicit_disjoint(selcx, impl2_def_id, impl1_def_id)
 }
 
 fn disjoint_with_filter<'cx, 'tcx>(

From e2567b034dd6847cc026eb80db47bd1271fe71de Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Fri, 21 Jan 2022 15:30:10 -0300
Subject: [PATCH 08/12] Remove intermediate function doesn't make more sense

---
 .../src/traits/coherence.rs                   | 39 ++++++-------------
 1 file changed, 11 insertions(+), 28 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index 178cff9501d73..4f3b08bd3add4 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -249,33 +249,6 @@ fn stable_disjoint<'cx, 'tcx>(
     param_env: ty::ParamEnv<'tcx>,
     impl1_header: &ty::ImplHeader<'tcx>,
     impl2_header: ty::ImplHeader<'tcx>,
-) -> bool {
-    let infcx = selcx.infcx();
-    let tcx = infcx.tcx;
-
-    disjoint_with_filter(selcx, param_env, impl1_header, impl2_header, |selcx, o| {
-        loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o)
-    })
-}
-
-fn strict_disjoint<'cx, 'tcx>(
-    selcx: &mut SelectionContext<'cx, 'tcx>,
-    impl1_def_id: DefId,
-    impl2_def_id: DefId,
-) -> bool {
-    explicit_disjoint(selcx, impl1_def_id, impl2_def_id)
-        || explicit_disjoint(selcx, impl2_def_id, impl1_def_id)
-}
-
-fn disjoint_with_filter<'cx, 'tcx>(
-    selcx: &mut SelectionContext<'cx, 'tcx>,
-    param_env: ty::ParamEnv<'tcx>,
-    impl1_header: &ty::ImplHeader<'tcx>,
-    impl2_header: ty::ImplHeader<'tcx>,
-    mut filter: impl FnMut(
-        &mut SelectionContext<'cx, 'tcx>,
-        &rustc_infer::traits::Obligation<'tcx, rustc_middle::ty::Predicate<'tcx>>,
-    ) -> bool,
 ) -> bool {
     debug!("overlap: impl1_header={:?}", impl1_header);
     debug!("overlap: impl2_header={:?}", impl2_header);
@@ -316,6 +289,7 @@ fn disjoint_with_filter<'cx, 'tcx>(
     // hold we need to check if `&'?a str: !Error` holds, if doesn't hold there's overlap because
     // at some point an impl for `&'?a str: Error` could be added.
     let infcx = selcx.infcx();
+    let tcx = infcx.tcx;
     let opt_failing_obligation = impl1_header
         .predicates
         .iter()
@@ -329,7 +303,7 @@ fn disjoint_with_filter<'cx, 'tcx>(
             predicate: p,
         })
         .chain(obligations)
-        .find(|o| filter(selcx, o));
+        .find(|o| loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o));
     // FIXME: the call to `selcx.predicate_may_hold_fatal` above should be ported
     // to the canonical trait query form, `infcx.predicate_may_hold`, once
     // the new system supports intercrate mode (which coherence needs).
@@ -344,6 +318,15 @@ fn disjoint_with_filter<'cx, 'tcx>(
 
 /// Given impl1 and impl2 check if both impls are never satisfied by a common type (including
 /// where-clauses) If so, return true, they are disjoint and false otherwise.
+fn strict_disjoint<'cx, 'tcx>(
+    selcx: &mut SelectionContext<'cx, 'tcx>,
+    impl1_def_id: DefId,
+    impl2_def_id: DefId,
+) -> bool {
+    explicit_disjoint(selcx, impl1_def_id, impl2_def_id)
+        || explicit_disjoint(selcx, impl2_def_id, impl1_def_id)
+}
+
 fn explicit_disjoint<'cx, 'tcx>(
     selcx: &mut SelectionContext<'cx, 'tcx>,
     impl1_def_id: DefId,

From e5f2fdb53939dc01ea6cad6e369c36aaa96f6e57 Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Sat, 22 Jan 2022 18:16:11 -0300
Subject: [PATCH 09/12] Restructure the code leveraging in abilities more than
 modes

---
 .../src/traits/coherence.rs                   | 98 +++++++++----------
 1 file changed, 47 insertions(+), 51 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index 4f3b08bd3add4..f22ca11d1c36e 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -11,7 +11,7 @@ use crate::traits::util::impl_trait_ref_and_oblig;
 use crate::traits::SkipLeakCheck;
 use crate::traits::{
     self, FulfillmentContext, Normalized, Obligation, ObligationCause, PredicateObligation,
-    SelectionContext,
+    PredicateObligations, SelectionContext,
 };
 use rustc_hir::def_id::{DefId, LOCAL_CRATE};
 use rustc_middle::ty::fast_reject::{self, SimplifyParams, StripReferences};
@@ -137,12 +137,23 @@ fn with_fresh_ty_vars<'cx, 'tcx>(
     header
 }
 
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
 enum OverlapMode {
     Stable,
     WithNegative,
     Strict,
 }
 
+impl OverlapMode {
+    fn use_negative_impl(&self) -> bool {
+        *self == OverlapMode::Strict || *self == OverlapMode::WithNegative
+    }
+
+    fn use_implicit_negative(&self) -> bool {
+        *self == OverlapMode::Stable || *self == OverlapMode::WithNegative
+    }
+}
+
 fn overlap_mode<'tcx>(tcx: TyCtxt<'tcx>, impl1_def_id: DefId, impl2_def_id: DefId) -> OverlapMode {
     if tcx.has_attr(impl1_def_id, sym::rustc_strict_coherence)
         != tcx.has_attr(impl2_def_id, sym::rustc_strict_coherence)
@@ -190,6 +201,16 @@ fn overlap_within_probe<'cx, 'tcx>(
     let infcx = selcx.infcx();
     let tcx = infcx.tcx;
 
+    let overlap_mode = overlap_mode(tcx, impl1_def_id, impl2_def_id);
+
+    if overlap_mode.use_negative_impl() {
+        if negative_impl(selcx, impl1_def_id, impl2_def_id)
+            || negative_impl(selcx, impl2_def_id, impl1_def_id)
+        {
+            return None;
+        }
+    }
+
     // For the purposes of this check, we don't bring any placeholder
     // types into scope; instead, we replace the generic types with
     // fresh type variables, and hence we do our evaluations in an
@@ -199,29 +220,15 @@ 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);
 
-    match overlap_mode(tcx, impl1_def_id, impl2_def_id) {
-        OverlapMode::Stable => {
-            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header) {
-                return None;
-            }
-        }
-        OverlapMode::Strict => {
-            if strict_disjoint(selcx, impl1_def_id, impl2_def_id) {
-                return None;
-            }
+    debug!("overlap: impl1_header={:?}", impl1_header);
+    debug!("overlap: impl2_header={:?}", impl2_header);
 
-            // Equate for error reporting
-            let _ = selcx
-                .infcx()
-                .at(&ObligationCause::dummy(), param_env)
-                .eq_impl_headers(&impl1_header, &impl2_header);
-        }
-        OverlapMode::WithNegative => {
-            if stable_disjoint(selcx, param_env, &impl1_header, impl2_header)
-                || strict_disjoint(selcx, impl1_def_id, impl2_def_id)
-            {
-                return None;
-            }
+    let obligations = equate_impl_headers(selcx, &impl1_header, &impl2_header)?;
+    debug!("overlap: unification check succeeded");
+
+    if overlap_mode.use_implicit_negative() {
+        if implicit_negative(selcx, param_env, &impl1_header, impl2_header, obligations) {
+            return None;
         }
     }
 
@@ -242,31 +249,29 @@ 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>,
+) -> Option<PredicateObligations<'tcx>> {
+    // Do `a` and `b` unify? If not, no overlap.
+    selcx
+        .infcx()
+        .at(&ObligationCause::dummy(), ty::ParamEnv::empty())
+        .eq_impl_headers(impl1_header, impl2_header)
+        .map(|infer_ok| infer_ok.obligations)
+        .ok()
+}
+
 /// Given impl1 and impl2 check if both impls can be satisfied by a common type (including
 /// where-clauses) If so, return false, otherwise return true, they are disjoint.
-fn stable_disjoint<'cx, 'tcx>(
+fn implicit_negative<'cx, 'tcx>(
     selcx: &mut SelectionContext<'cx, 'tcx>,
     param_env: ty::ParamEnv<'tcx>,
     impl1_header: &ty::ImplHeader<'tcx>,
     impl2_header: ty::ImplHeader<'tcx>,
+    obligations: PredicateObligations<'tcx>,
 ) -> bool {
-    debug!("overlap: impl1_header={:?}", impl1_header);
-    debug!("overlap: impl2_header={:?}", impl2_header);
-
-    // Do `a` and `b` unify? If not, no overlap.
-    let obligations = match selcx
-        .infcx()
-        .at(&ObligationCause::dummy(), param_env)
-        .eq_impl_headers(&impl1_header, &impl2_header)
-    {
-        Ok(InferOk { obligations, value: () }) => obligations,
-        Err(_) => {
-            return true;
-        }
-    };
-
-    debug!("overlap: unification check succeeded");
-
     // There's no overlap if obligations are unsatisfiable or if the obligation negated is
     // satisfied.
     //
@@ -318,16 +323,7 @@ fn stable_disjoint<'cx, 'tcx>(
 
 /// Given impl1 and impl2 check if both impls are never satisfied by a common type (including
 /// where-clauses) If so, return true, they are disjoint and false otherwise.
-fn strict_disjoint<'cx, 'tcx>(
-    selcx: &mut SelectionContext<'cx, 'tcx>,
-    impl1_def_id: DefId,
-    impl2_def_id: DefId,
-) -> bool {
-    explicit_disjoint(selcx, impl1_def_id, impl2_def_id)
-        || explicit_disjoint(selcx, impl2_def_id, impl1_def_id)
-}
-
-fn explicit_disjoint<'cx, 'tcx>(
+fn negative_impl<'cx, 'tcx>(
     selcx: &mut SelectionContext<'cx, 'tcx>,
     impl1_def_id: DefId,
     impl2_def_id: DefId,

From 7847ca8c61f7dc49775f237efae9c7da007d20af Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Sat, 22 Jan 2022 21:24:11 -0300
Subject: [PATCH 10/12] Document OverlapMode

---
 compiler/rustc_trait_selection/src/traits/coherence.rs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index f22ca11d1c36e..abe51b3fe302f 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -137,10 +137,15 @@ fn with_fresh_ty_vars<'cx, 'tcx>(
     header
 }
 
+/// What kind of overlap check are we doing -- this exists just for testing and feature-gating
+/// purposes.
 #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
 enum OverlapMode {
+    /// The 1.0 rules (either types fail to unify, or where clauses are not implemented for crate-local types)
     Stable,
+    /// Feature-gated test: Stable, *or* there is an explicit negative impl that rules out one of the where-clauses.
     WithNegative,
+    /// Just check for negative impls, not for "where clause not implemented": used for testing.
     Strict,
 }
 

From 269383226f8f11e21883590d40270bdd58339477 Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Sat, 22 Jan 2022 21:25:56 -0300
Subject: [PATCH 11/12] Rename strict_check to negative_impl_exists

---
 .../rustc_trait_selection/src/traits/coherence.rs    | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index abe51b3fe302f..d1a966455f0b2 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -313,7 +313,9 @@ fn implicit_negative<'cx, 'tcx>(
             predicate: p,
         })
         .chain(obligations)
-        .find(|o| loose_check(selcx, o) || tcx.features().negative_impls && strict_check(selcx, o));
+        .find(|o| {
+            loose_check(selcx, o) || tcx.features().negative_impls && negative_impl_exists(selcx, o)
+        });
     // FIXME: the call to `selcx.predicate_may_hold_fatal` above should be ported
     // to the canonical trait query form, `infcx.predicate_may_hold`, once
     // the new system supports intercrate mode (which coherence needs).
@@ -377,8 +379,10 @@ fn negative_impl<'cx, 'tcx>(
             }
         };
 
-        let opt_failing_obligation =
-            obligations.into_iter().chain(more_obligations).find(|o| strict_check(selcx, o));
+        let opt_failing_obligation = obligations
+            .into_iter()
+            .chain(more_obligations)
+            .find(|o| negative_impl_exists(selcx, o));
 
         if let Some(failing_obligation) = opt_failing_obligation {
             debug!("overlap: obligation unsatisfiable {:?}", failing_obligation);
@@ -396,7 +400,7 @@ fn loose_check<'cx, 'tcx>(
     !selcx.predicate_may_hold_fatal(o)
 }
 
-fn strict_check<'cx, 'tcx>(
+fn negative_impl_exists<'cx, 'tcx>(
     selcx: &SelectionContext<'cx, 'tcx>,
     o: &PredicateObligation<'tcx>,
 ) -> bool {

From 8189bac9636930155768150886e28e221523d6ac Mon Sep 17 00:00:00 2001
From: Santiago Pastorino <spastorino@gmail.com>
Date: Sat, 22 Jan 2022 21:28:12 -0300
Subject: [PATCH 12/12] FIXME include regions too

---
 compiler/rustc_trait_selection/src/traits/coherence.rs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/compiler/rustc_trait_selection/src/traits/coherence.rs b/compiler/rustc_trait_selection/src/traits/coherence.rs
index d1a966455f0b2..80ed9023d9694 100644
--- a/compiler/rustc_trait_selection/src/traits/coherence.rs
+++ b/compiler/rustc_trait_selection/src/traits/coherence.rs
@@ -408,7 +408,10 @@ fn negative_impl_exists<'cx, 'tcx>(
     let tcx = infcx.tcx;
     o.flip_polarity(tcx)
         .as_ref()
-        .map(|o| selcx.infcx().predicate_must_hold_modulo_regions(o))
+        .map(|o| {
+            // FIXME This isn't quite correct, regions should be included
+            selcx.infcx().predicate_must_hold_modulo_regions(o)
+        })
         .unwrap_or(false)
 }