@@ -589,7 +589,7 @@ impl<'tcx> RegionInferenceContext<'tcx> {
589589 fn check_type_tests (
590590 & self ,
591591 infcx : & InferCtxt < ' tcx > ,
592- mut propagated_outlives_requirements : Option < & mut Vec < ClosureOutlivesRequirement < ' tcx > > > ,
592+ propagated_outlives_requirements : Option < & mut Vec < ClosureOutlivesRequirement < ' tcx > > > ,
593593 errors_buffer : & mut RegionErrors < ' tcx > ,
594594 ) {
595595 let tcx = infcx. tcx ;
@@ -599,6 +599,9 @@ impl<'tcx> RegionInferenceContext<'tcx> {
599599 // the user. Avoid that.
600600 let mut deduplicate_errors = FxIndexSet :: default ( ) ;
601601
602+ let mut conjunctive_propagated_outlives_requirements =
603+ propagated_outlives_requirements. is_some ( ) . then_some ( vec ! [ ] ) ;
604+
602605 for type_test in & self . type_tests {
603606 debug ! ( "check_type_test: {:?}" , type_test) ;
604607
@@ -612,8 +615,13 @@ impl<'tcx> RegionInferenceContext<'tcx> {
612615 continue ;
613616 }
614617
615- if let Some ( propagated_outlives_requirements) = & mut propagated_outlives_requirements
616- && self . try_promote_type_test ( infcx, type_test, propagated_outlives_requirements)
618+ if let Some ( conjunctive_propagated_outlives_requirements) =
619+ & mut conjunctive_propagated_outlives_requirements
620+ && self . try_promote_type_test (
621+ infcx,
622+ type_test,
623+ conjunctive_propagated_outlives_requirements,
624+ )
617625 {
618626 continue ;
619627 }
@@ -637,6 +645,69 @@ impl<'tcx> RegionInferenceContext<'tcx> {
637645 errors_buffer. push ( RegionErrorKind :: TypeTestError { type_test : type_test. clone ( ) } ) ;
638646 }
639647 }
648+
649+ if let Some ( mut conjunctive_requirements) = conjunctive_propagated_outlives_requirements
650+ && !conjunctive_requirements. is_empty ( )
651+ {
652+ // We can simplify this list of list of requirements.
653+ //
654+ // Say we did some number of type tests and it results in following requirements:
655+ //
656+ // R1: (T: 'a OR T: 'b)
657+ // R2: (T: 'a)
658+ //
659+ // * See `try_promote_type_test` below on why we obtain OR requirements implicitly.
660+ //
661+ // Full requirement is then: R1 AND R2. *BUT*, we can remove R1 entirely, because we already
662+ // require `T: 'a`, which implies `T:'a OR T: 'b`, making R1 redundant.
663+ //
664+ // The requirements can be seen as a boolean conjunctive normal form expression:
665+ // Treat a requirement `T: 'region` as a boolean value, then this problem is (almost)
666+ // equivalant to "Unit Propagation". However, this problem we are trying to solve is much
667+ // simpler: Unit Propagation considers any form of subexpression, even containing negation
668+ // of values, making it a multi-pass algorithm. The only subexpressions we encounter are of
669+ // the form (R1 OR ... OR RN), thus if even on R is required on their own (a unit), this
670+ // whole subexpression can be removed.
671+ //
672+ // So we can filter redundant OR requirements with the following algorithm:
673+ // Collect every Unit requirement. Then for every other requirement, if one of the units is
674+ // contained within them we can remove the entire requirement from the list.
675+
676+ fn requirement_key < ' a > ( subject : ClosureOutlivesRequirement < ' a > ) -> ( Ty < ' a > , RegionVid ) {
677+ let ClosureOutlivesSubject :: Ty ( ClosureOutlivesSubjectTy { inner : ty } ) =
678+ subject. subject
679+ else {
680+ unreachable ! ( "ClosureOutliveSubject of a type test is always a Ty" ) ;
681+ } ;
682+ ( ty, subject. outlived_free_region )
683+ }
684+
685+ let units: Vec < _ > = conjunctive_requirements
686+ . iter ( )
687+ . filter_map ( |r| {
688+ let [ r] = r. as_slice ( ) else { return None } ;
689+ Some ( requirement_key ( * r) )
690+ } )
691+ . collect ( ) ;
692+
693+ // Remove the `or_requirement`s that contain any of the unit requirements.
694+ conjunctive_requirements. retain ( |or_requirement| {
695+ or_requirement. len ( ) == 1
696+ || !or_requirement. iter ( ) . any ( |r| {
697+ let key = requirement_key ( * r) ;
698+ units. contains ( & key)
699+ } )
700+ } ) ;
701+
702+ assert ! (
703+ !conjunctive_requirements. is_empty( ) ,
704+ "It should not be possible to remove every requirement."
705+ ) ;
706+ // Propagate all requirements as is.
707+ propagated_outlives_requirements
708+ . expect ( "conjunctive_requirements is `Some`, so this should be as well" )
709+ . extend ( conjunctive_requirements. into_iter ( ) . flatten ( ) ) ;
710+ }
640711 }
641712
642713 /// Invoked when we have some type-test (e.g., `T: 'X`) that we cannot
@@ -668,7 +739,7 @@ impl<'tcx> RegionInferenceContext<'tcx> {
668739 & self ,
669740 infcx : & InferCtxt < ' tcx > ,
670741 type_test : & TypeTest < ' tcx > ,
671- propagated_outlives_requirements : & mut Vec < ClosureOutlivesRequirement < ' tcx > > ,
742+ propagated_outlives_requirements : & mut Vec < Vec < ClosureOutlivesRequirement < ' tcx > > > ,
672743 ) -> bool {
673744 let tcx = infcx. tcx ;
674745 let TypeTest { generic_kind, lower_bound, span : blame_span, verify_bound : _ } = * type_test;
@@ -694,58 +765,55 @@ impl<'tcx> RegionInferenceContext<'tcx> {
694765 if let Some ( p) = self . scc_values . placeholders_contained_in ( r_scc) . next ( ) {
695766 debug ! ( "encountered placeholder in higher universe: {:?}, requiring 'static" , p) ;
696767 let static_r = self . universal_regions ( ) . fr_static ;
697- propagated_outlives_requirements. push ( ClosureOutlivesRequirement {
768+ propagated_outlives_requirements. push ( vec ! [ ClosureOutlivesRequirement {
698769 subject,
699770 outlived_free_region: static_r,
700771 blame_span,
701772 category: ConstraintCategory :: Boring ,
702- } ) ;
773+ } ] ) ;
703774
704775 // we can return here -- the code below might push add'l constraints
705776 // but they would all be weaker than this one.
706777 return true ;
707778 }
708779
780+ let universal_regions: Vec < _ > =
781+ self . scc_values . universal_regions_outlived_by ( r_scc) . collect ( ) ;
782+ debug ! ( ?universal_regions) ;
783+
784+ // Filter to only the "minimal" universal regions:
785+ // Drop any region `a` that strictly outlives another region `b`.
786+ let minimal_universal_regions: Vec < _ > = universal_regions
787+ . iter ( )
788+ . copied ( )
789+ . filter ( |& a| {
790+ !universal_regions. iter ( ) . copied ( ) . any ( |b| {
791+ !self . universal_region_relations . outlives ( a, b)
792+ && self . universal_region_relations . outlives ( b, a)
793+ } )
794+ } )
795+ . collect ( ) ;
796+
797+ assert ! (
798+ !minimal_universal_regions. is_empty( ) ,
799+ "There should always be at least 1 minimal region"
800+ ) ;
801+
709802 // For each region outlived by lower_bound find a non-local,
710803 // universal region (it may be the same region) and add it to
711804 // `ClosureOutlivesRequirement`.
712805 let mut found_outlived_universal_region = false ;
713- for ur in self . scc_values . universal_regions_outlived_by ( r_scc ) {
806+ for ur in minimal_universal_regions {
714807 found_outlived_universal_region = true ;
715808 debug ! ( "universal_region_outlived_by ur={:?}" , ur) ;
716- let mut non_local_ub = self . universal_region_relations . non_local_upper_bounds ( ur) ;
809+ let non_local_ub = self . universal_region_relations . non_local_upper_bounds ( ur) ;
717810 debug ! ( ?non_local_ub) ;
718811
719- // We don't need to propagate every `T: 'ub` for soundness:
720- // Say we have the following outlives constraints given (`'b: 'a` == `a -> b`):
721- //
722- // a
723- // \
724- // -> c
725- // /
726- // b
727- //
728- // And we are doing the type test `T: 'a`.
729- //
730- // The `lower_bound_universal_regions` of `'a` are `['a, 'c]`. The `upper_bounds` of `'a`
731- // is `['a]`, so we propagate `T: 'a`.
732- // The `upper_bounds` of `'c` are `['a, 'b]`, propagating `T: 'a` is correct;
733- // `T: 'b` is redundant because it provides no value to proving `T: 'a`.
734- //
735- // So we filter the set of upper_bounds to regions already outliving `lower_bound`,
736- // but if this subset is empty, we fall back to the original one.
737- let subset: Vec < _ > = non_local_ub
738- . iter ( )
739- . copied ( )
740- . filter ( |ub| self . eval_outlives ( * ub, lower_bound) )
741- . collect ( ) ;
742- non_local_ub = if subset. is_empty ( ) { non_local_ub } else { subset } ;
743- debug ! ( ?non_local_ub, "upper_bounds after filtering" ) ;
744-
745812 // This is slightly too conservative. To show T: '1, given `'2: '1`
746813 // and `'3: '1` we only need to prove that T: '2 *or* T: '3, but to
747814 // avoid potential non-determinism we approximate this by requiring
748815 // T: '1 and T: '2.
816+ let mut or_requirements = Vec :: with_capacity ( non_local_ub. len ( ) ) ;
749817 for upper_bound in non_local_ub {
750818 debug_assert ! ( self . universal_regions( ) . is_universal_region( upper_bound) ) ;
751819 debug_assert ! ( !self . universal_regions( ) . is_local_free_region( upper_bound) ) ;
@@ -757,8 +825,9 @@ impl<'tcx> RegionInferenceContext<'tcx> {
757825 category : ConstraintCategory :: Boring ,
758826 } ;
759827 debug ! ( ?requirement, "adding closure requirement" ) ;
760- propagated_outlives_requirements . push ( requirement) ;
828+ or_requirements . push ( requirement) ;
761829 }
830+ propagated_outlives_requirements. push ( or_requirements) ;
762831 }
763832 // If we succeed to promote the subject, i.e. it only contains non-local regions,
764833 // and fail to prove the type test inside of the closure, the `lower_bound` has to
0 commit comments