From c224982825cfbc3ead20c993ad1f4d1cfe8d043e Mon Sep 17 00:00:00 2001
From: Ziqiao Zhou <ziqiaozhou@microsoft.com>
Date: Tue, 29 Oct 2024 12:59:39 -0700
Subject: [PATCH] Do not skip Box by adding with_negative_coherence

---
 source/rust_verify/src/lifetime.rs          | 1 +
 source/rust_verify/src/lifetime_generate.rs | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/source/rust_verify/src/lifetime.rs b/source/rust_verify/src/lifetime.rs
index 45cc422d6..f441788bd 100644
--- a/source/rust_verify/src/lifetime.rs
+++ b/source/rust_verify/src/lifetime.rs
@@ -205,6 +205,7 @@ pub(crate) fn check<'tcx>(queries: &'tcx rustc_interface::Queries<'tcx>) {
 
 const PRELUDE: &str = "\
 #![feature(negative_impls)]
+#![feature(with_negative_coherence)]
 #![feature(box_patterns)]
 #![feature(ptr_metadata)]
 #![feature(never_type)]
diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs
index 5f75eef2a..aa0cfff50 100644
--- a/source/rust_verify/src/lifetime_generate.rs
+++ b/source/rust_verify/src/lifetime_generate.rs
@@ -2263,7 +2263,7 @@ fn erase_impl_assocs<'tcx>(ctxt: &Context<'tcx>, state: &mut State, impl_id: Def
     // v1.80 stablized Iterator and IntoIterator for Box.
     // It needs to implement !Iterartor to avoid conflicts.
     // The lifetime checking does not reserve polarity.
-    if matches!(name.raw_id.as_str(), "Iterator" | "IntoIterator") {
+    /*if matches!(name.raw_id.as_str(), "Iterator" | "IntoIterator") {
         let skip = match self_typ.as_ref() {
             // found both positive and negative implementation of trait `T55_Iterator` for type `&mut std::boxed::Box<[_], _>
             TypX::Ref(r, ..) => {
@@ -2280,7 +2280,7 @@ fn erase_impl_assocs<'tcx>(ctxt: &Context<'tcx>, state: &mut State, impl_id: Def
             println!("skip  = {:?} {:?} {:?}", self_typ, trait_polarity, name);
             return;
         }
-    }
+    }*/
 
     state.trait_impls.push(trait_impl);
 }