@@ -23,7 +23,7 @@ use rustc_middle::traits::specialization_graph::OverlapMode;
23
23
use rustc_middle:: traits:: DefiningAnchor ;
24
24
use rustc_middle:: ty:: fast_reject:: { DeepRejectCtxt , TreatParams } ;
25
25
use rustc_middle:: ty:: visit:: { TypeVisitable , TypeVisitableExt } ;
26
- use rustc_middle:: ty:: { self , ImplSubject , Ty , TyCtxt , TypeVisitor } ;
26
+ use rustc_middle:: ty:: { self , Ty , TyCtxt , TypeVisitor } ;
27
27
use rustc_span:: symbol:: sym;
28
28
use rustc_span:: DUMMY_SP ;
29
29
use std:: fmt:: Debug ;
@@ -170,8 +170,8 @@ fn overlap<'tcx>(
170
170
overlap_mode : OverlapMode ,
171
171
) -> Option < OverlapResult < ' tcx > > {
172
172
if overlap_mode. use_negative_impl ( ) {
173
- if negative_impl ( tcx, impl1_def_id, impl2_def_id)
174
- || negative_impl ( tcx, impl2_def_id, impl1_def_id)
173
+ if impl_intersection_has_negative_obligation ( tcx, impl1_def_id, impl2_def_id)
174
+ || impl_intersection_has_negative_obligation ( tcx, impl2_def_id, impl1_def_id)
175
175
{
176
176
return None ;
177
177
}
@@ -198,13 +198,21 @@ fn overlap<'tcx>(
198
198
let impl1_header = with_fresh_ty_vars ( selcx, param_env, impl1_def_id) ;
199
199
let impl2_header = with_fresh_ty_vars ( selcx, param_env, impl2_def_id) ;
200
200
201
- let obligations = equate_impl_headers ( selcx. infcx , & impl1_header, & impl2_header) ?;
201
+ // Equate the headers to find their intersection (the general type, with infer vars,
202
+ // that may apply both impls).
203
+ let equate_obligations = equate_impl_headers ( selcx. infcx , & impl1_header, & impl2_header) ?;
202
204
debug ! ( "overlap: unification check succeeded" ) ;
203
205
204
- if overlap_mode. use_implicit_negative ( ) {
205
- if implicit_negative ( selcx, param_env, & impl1_header, impl2_header, obligations) {
206
- return None ;
207
- }
206
+ if overlap_mode. use_implicit_negative ( )
207
+ && impl_intersection_has_impossible_obligation (
208
+ selcx,
209
+ param_env,
210
+ & impl1_header,
211
+ impl2_header,
212
+ equate_obligations,
213
+ )
214
+ {
215
+ return None ;
208
216
}
209
217
210
218
// We toggle the `leak_check` by using `skip_leak_check` when constructing the
@@ -250,52 +258,38 @@ fn equate_impl_headers<'tcx>(
250
258
result. map ( |infer_ok| infer_ok. obligations ) . ok ( )
251
259
}
252
260
253
- /// Given impl1 and impl2 check if both impls can be satisfied by a common type (including
254
- /// where-clauses) If so, return false, otherwise return true, they are disjoint.
255
- fn implicit_negative < ' cx , ' tcx > (
261
+ /// Check if both impls can be satisfied by a common type by considering whether
262
+ /// any of either impl's obligations is not known to hold.
263
+ ///
264
+ /// For example, given these two impls:
265
+ /// `impl From<MyLocalType> for Box<dyn Error>` (in my crate)
266
+ /// `impl<E> From<E> for Box<dyn Error> where E: Error` (in libstd)
267
+ ///
268
+ /// After replacing both impl headers with inference vars (which happens before
269
+ /// this function is called), we get:
270
+ /// `Box<dyn Error>: From<MyLocalType>`
271
+ /// `Box<dyn Error>: From<?E>`
272
+ ///
273
+ /// This gives us `?E = MyLocalType`. We then certainly know that `MyLocalType: Error`
274
+ /// never holds in intercrate mode since a local impl does not exist, and a
275
+ /// downstream impl cannot be added -- therefore can consider the intersection
276
+ /// of the two impls above to be empty.
277
+ ///
278
+ /// Importantly, this works even if there isn't a `impl !Error for MyLocalType`.
279
+ fn impl_intersection_has_impossible_obligation < ' cx , ' tcx > (
256
280
selcx : & mut SelectionContext < ' cx , ' tcx > ,
257
281
param_env : ty:: ParamEnv < ' tcx > ,
258
282
impl1_header : & ty:: ImplHeader < ' tcx > ,
259
283
impl2_header : ty:: ImplHeader < ' tcx > ,
260
284
obligations : PredicateObligations < ' tcx > ,
261
285
) -> bool {
262
- // There's no overlap if obligations are unsatisfiable or if the obligation negated is
263
- // satisfied.
264
- //
265
- // For example, given these two impl headers:
266
- //
267
- // `impl<'a> From<&'a str> for Box<dyn Error>`
268
- // `impl<E> From<E> for Box<dyn Error> where E: Error`
269
- //
270
- // So we have:
271
- //
272
- // `Box<dyn Error>: From<&'?a str>`
273
- // `Box<dyn Error>: From<?E>`
274
- //
275
- // After equating the two headers:
276
- //
277
- // `Box<dyn Error> = Box<dyn Error>`
278
- // So, `?E = &'?a str` and then given the where clause `&'?a str: Error`.
279
- //
280
- // If the obligation `&'?a str: Error` holds, it means that there's overlap. If that doesn't
281
- // hold we need to check if `&'?a str: !Error` holds, if doesn't hold there's overlap because
282
- // at some point an impl for `&'?a str: Error` could be added.
283
- debug ! (
284
- "implicit_negative(impl1_header={:?}, impl2_header={:?}, obligations={:?})" ,
285
- impl1_header, impl2_header, obligations
286
- ) ;
287
286
let infcx = selcx. infcx ;
288
- let opt_failing_obligation = impl1_header
289
- . predicates
290
- . iter ( )
291
- . copied ( )
292
- . chain ( impl2_header. predicates )
293
- . map ( |p| infcx. resolve_vars_if_possible ( p) )
294
- . map ( |p| Obligation {
295
- cause : ObligationCause :: dummy ( ) ,
296
- param_env,
297
- recursion_depth : 0 ,
298
- predicate : p,
287
+
288
+ let opt_failing_obligation = [ & impl1_header. predicates , & impl2_header. predicates ]
289
+ . into_iter ( )
290
+ . flatten ( )
291
+ . map ( |& predicate| {
292
+ Obligation :: new ( infcx. tcx , ObligationCause :: dummy ( ) , param_env, predicate)
299
293
} )
300
294
. chain ( obligations)
301
295
. find ( |o| !selcx. predicate_may_hold_fatal ( o) ) ;
@@ -308,9 +302,27 @@ fn implicit_negative<'cx, 'tcx>(
308
302
}
309
303
}
310
304
311
- /// Given impl1 and impl2 check if both impls are never satisfied by a common type (including
312
- /// where-clauses) If so, return true, they are disjoint and false otherwise.
313
- fn negative_impl ( tcx : TyCtxt < ' _ > , impl1_def_id : DefId , impl2_def_id : DefId ) -> bool {
305
+ /// Check if both impls can be satisfied by a common type by considering whether
306
+ /// any of first impl's obligations is known not to hold *via a negative predicate*.
307
+ ///
308
+ /// For example, given these two impls:
309
+ /// `struct MyCustomBox<T: ?Sized>(Box<T>);`
310
+ /// `impl From<&str> for MyCustomBox<dyn Error>` (in my crate)
311
+ /// `impl<E> From<E> for MyCustomBox<dyn Error> where E: Error` (in my crate)
312
+ ///
313
+ /// After replacing the second impl's header with inference vars, we get:
314
+ /// `MyCustomBox<dyn Error>: From<&str>`
315
+ /// `MyCustomBox<dyn Error>: From<?E>`
316
+ ///
317
+ /// This gives us `?E = &str`. We then try to prove the first impl's predicates
318
+ /// after negating, giving us `&str: !Error`. This is a negative impl provided by
319
+ /// libstd, and therefore we can guarantee for certain that libstd will never add
320
+ /// a positive impl for `&str: Error` (without it being a breaking change).
321
+ fn impl_intersection_has_negative_obligation (
322
+ tcx : TyCtxt < ' _ > ,
323
+ impl1_def_id : DefId ,
324
+ impl2_def_id : DefId ,
325
+ ) -> bool {
314
326
debug ! ( "negative_impl(impl1_def_id={:?}, impl2_def_id={:?})" , impl1_def_id, impl2_def_id) ;
315
327
316
328
// Create an infcx, taking the predicates of impl1 as assumptions:
@@ -336,57 +348,45 @@ fn negative_impl(tcx: TyCtxt<'_>, impl1_def_id: DefId, impl2_def_id: DefId) -> b
336
348
// Attempt to prove that impl2 applies, given all of the above.
337
349
let selcx = & mut SelectionContext :: new ( & infcx) ;
338
350
let impl2_substs = infcx. fresh_substs_for_item ( DUMMY_SP , impl2_def_id) ;
339
- let ( subject2, obligations ) =
351
+ let ( subject2, normalization_obligations ) =
340
352
impl_subject_and_oblig ( selcx, impl_env, impl2_def_id, impl2_substs, |_, _| {
341
353
ObligationCause :: dummy ( )
342
354
} ) ;
343
355
344
- !equate ( & infcx, impl_env, subject1, subject2, obligations, impl1_def_id)
345
- }
346
-
347
- fn equate < ' tcx > (
348
- infcx : & InferCtxt < ' tcx > ,
349
- impl_env : ty:: ParamEnv < ' tcx > ,
350
- subject1 : ImplSubject < ' tcx > ,
351
- subject2 : ImplSubject < ' tcx > ,
352
- obligations : impl Iterator < Item = PredicateObligation < ' tcx > > ,
353
- body_def_id : DefId ,
354
- ) -> bool {
355
- // do the impls unify? If not, not disjoint.
356
- let Ok ( InferOk { obligations : more_obligations, .. } ) =
356
+ // do the impls unify? If not, then it's not currently possible to prove any
357
+ // obligations about their intersection.
358
+ let Ok ( InferOk { obligations : equate_obligations, .. } ) =
357
359
infcx. at ( & ObligationCause :: dummy ( ) , impl_env) . eq ( DefineOpaqueTypes :: No , subject1, subject2)
358
360
else {
359
361
debug ! ( "explicit_disjoint: {:?} does not unify with {:?}" , subject1, subject2) ;
360
- return true ;
362
+ return false ;
361
363
} ;
362
364
363
- let opt_failing_obligation = obligations
364
- . into_iter ( )
365
- . chain ( more_obligations)
366
- . find ( |o| negative_impl_exists ( infcx, o, body_def_id) ) ;
367
-
368
- if let Some ( failing_obligation) = opt_failing_obligation {
369
- debug ! ( "overlap: obligation unsatisfiable {:?}" , failing_obligation) ;
370
- false
371
- } else {
372
- true
365
+ for obligation in normalization_obligations. into_iter ( ) . chain ( equate_obligations) {
366
+ if negative_impl_exists ( & infcx, & obligation, impl1_def_id) {
367
+ debug ! ( "overlap: obligation unsatisfiable {:?}" , obligation) ;
368
+ return true ;
369
+ }
373
370
}
371
+
372
+ false
374
373
}
375
374
376
- /// Try to prove that a negative impl exist for the given obligation and its super predicates.
375
+ /// Try to prove that a negative impl exist for the obligation or its supertraits.
376
+ ///
377
+ /// If such a negative impl exists, then the obligation definitely must not hold
378
+ /// due to coherence, even if it's not necessarily "knowable" in this crate. Any
379
+ /// valid impl downstream would not be able to exist due to the overlapping
380
+ /// negative impl.
377
381
#[ instrument( level = "debug" , skip( infcx) ) ]
378
382
fn negative_impl_exists < ' tcx > (
379
383
infcx : & InferCtxt < ' tcx > ,
380
384
o : & PredicateObligation < ' tcx > ,
381
385
body_def_id : DefId ,
382
386
) -> bool {
383
- if resolve_negative_obligation ( infcx. fork ( ) , o, body_def_id) {
384
- return true ;
385
- }
386
-
387
387
// Try to prove a negative obligation exists for super predicates
388
388
for pred in util:: elaborate ( infcx. tcx , iter:: once ( o. predicate ) ) {
389
- if resolve_negative_obligation ( infcx. fork ( ) , & o. with ( infcx. tcx , pred) , body_def_id) {
389
+ if prove_negated_obligation ( infcx. fork ( ) , & o. with ( infcx. tcx , pred) , body_def_id) {
390
390
return true ;
391
391
}
392
392
}
@@ -395,7 +395,7 @@ fn negative_impl_exists<'tcx>(
395
395
}
396
396
397
397
#[ instrument( level = "debug" , skip( infcx) ) ]
398
- fn resolve_negative_obligation < ' tcx > (
398
+ fn prove_negated_obligation < ' tcx > (
399
399
infcx : InferCtxt < ' tcx > ,
400
400
o : & PredicateObligation < ' tcx > ,
401
401
body_def_id : DefId ,
0 commit comments