@@ -585,7 +585,7 @@ impl<'tcx> RegionInferenceContext<'tcx> {
585585 fn check_type_tests (
586586 & self ,
587587 infcx : & InferCtxt < ' tcx > ,
588- mut propagated_outlives_requirements : Option < & mut Vec < ClosureOutlivesRequirement < ' tcx > > > ,
588+ propagated_outlives_requirements : Option < & mut Vec < ClosureOutlivesRequirement < ' tcx > > > ,
589589 errors_buffer : & mut RegionErrors < ' tcx > ,
590590 ) {
591591 let tcx = infcx. tcx ;
@@ -595,6 +595,13 @@ impl<'tcx> RegionInferenceContext<'tcx> {
595595 // the user. Avoid that.
596596 let mut deduplicate_errors = FxIndexSet :: default ( ) ;
597597
598+ // Each type test introduces one or more OR-constraints (e.g. T: 'a OR T: 'b),
599+ // where at least one option in each constraint must be satisfied. All such
600+ // constraints must be satisfied simultaneously: i.e., they form a conjunction (AND).
601+ // We'll use this conjunctive requirement later on.
602+ let mut conjunctive_propagated_outlives_requirement =
603+ propagated_outlives_requirements. is_some ( ) . then_some ( vec ! [ ] ) ;
604+
598605 for type_test in & self . type_tests {
599606 debug ! ( "check_type_test: {:?}" , type_test) ;
600607
@@ -608,8 +615,13 @@ impl<'tcx> RegionInferenceContext<'tcx> {
608615 continue ;
609616 }
610617
611- if let Some ( propagated_outlives_requirements) = & mut propagated_outlives_requirements
612- && self . try_promote_type_test ( infcx, type_test, propagated_outlives_requirements)
618+ if let Some ( conjunctive_propagated_outlives_requirements) =
619+ & mut conjunctive_propagated_outlives_requirement
620+ && self . try_promote_type_test (
621+ infcx,
622+ type_test,
623+ conjunctive_propagated_outlives_requirements,
624+ )
613625 {
614626 continue ;
615627 }
@@ -633,6 +645,85 @@ impl<'tcx> RegionInferenceContext<'tcx> {
633645 errors_buffer. push ( RegionErrorKind :: TypeTestError { type_test : type_test. clone ( ) } ) ;
634646 }
635647 }
648+
649+ if let Some ( mut conjunctive_requirement) = conjunctive_propagated_outlives_requirement
650+ && !conjunctive_requirement. 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+ // equivalent 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+ // Because of the outlives relations, we can actually have a stronger redundancy check,
673+ // say we have following requirements that create a conjunctive requirement:
674+ // R1: T: 'a
675+ // R2: T: 'b OR T: 'c
676+ // R: R1 AND R2
677+ //
678+ // And we have we an assumption in our environment that `'a: 'b`, we can thus remove R2
679+ // as well. `T: 'b` is implied by `T: 'a` because of the assumption `'a: 'b`:
680+ // T -> 'a -> 'b
681+ //
682+ // So we can filter redundant OR requirements with the following algorithm:
683+ // Collect every Unit requirement. Then for every OR requirement, loop over its
684+ // individual requirements and if the region is outlived by the region of one of the
685+ // units, remove the entire OR requirement.
686+
687+ fn requirement_key < ' a > ( subject : ClosureOutlivesRequirement < ' a > ) -> ( Ty < ' a > , RegionVid ) {
688+ let ClosureOutlivesSubject :: Ty ( ClosureOutlivesSubjectTy { inner : ty } ) =
689+ subject. subject
690+ else {
691+ unreachable ! ( "ClosureOutliveSubject of a type test is always a Ty" ) ;
692+ } ;
693+ ( ty, subject. outlived_free_region )
694+ }
695+
696+ let units: Vec < _ > = conjunctive_requirement
697+ . iter ( )
698+ . filter_map ( |r| {
699+ let [ r] = r. as_slice ( ) else { return None } ;
700+ Some ( requirement_key ( * r) )
701+ } )
702+ . collect ( ) ;
703+
704+ // Remove the `or_requirement`s that contain any of the unit requirements.
705+ conjunctive_requirement. retain ( |or_requirement| {
706+ or_requirement. len ( ) == 1
707+ || !or_requirement. iter ( ) . any ( |r| {
708+ let ( ty, region) = requirement_key ( * r) ;
709+ units. iter ( ) . any ( |& ( unit_subj, unit_region) | {
710+ // Same type, and the unit region outlives the disjunct region,
711+ // meaning T: unit_region implies T: region.
712+ unit_subj == ty
713+ && self . universal_region_relations . outlives ( unit_region, region)
714+ } )
715+ } )
716+ } ) ;
717+
718+ assert ! (
719+ !conjunctive_requirement. is_empty( ) ,
720+ "It should not be possible to remove every requirement."
721+ ) ;
722+ // Propagate all requirements as is.
723+ propagated_outlives_requirements
724+ . expect ( "conjunctive_requirements is `Some`, so this should be as well" )
725+ . extend ( conjunctive_requirement. into_iter ( ) . flatten ( ) ) ;
726+ }
636727 }
637728
638729 /// Invoked when we have some type-test (e.g., `T: 'X`) that we cannot
@@ -664,7 +755,7 @@ impl<'tcx> RegionInferenceContext<'tcx> {
664755 & self ,
665756 infcx : & InferCtxt < ' tcx > ,
666757 type_test : & TypeTest < ' tcx > ,
667- propagated_outlives_requirements : & mut Vec < ClosureOutlivesRequirement < ' tcx > > ,
758+ propagated_outlives_requirements : & mut Vec < Vec < ClosureOutlivesRequirement < ' tcx > > > ,
668759 ) -> bool {
669760 let tcx = infcx. tcx ;
670761 let TypeTest { generic_kind, lower_bound, span : blame_span, verify_bound : _ } = * type_test;
@@ -690,24 +781,41 @@ impl<'tcx> RegionInferenceContext<'tcx> {
690781 if let Some ( p) = self . scc_values . placeholders_contained_in ( r_scc) . next ( ) {
691782 debug ! ( "encountered placeholder in higher universe: {:?}, requiring 'static" , p) ;
692783 let static_r = self . universal_regions ( ) . fr_static ;
693- propagated_outlives_requirements. push ( ClosureOutlivesRequirement {
784+ propagated_outlives_requirements. push ( vec ! [ ClosureOutlivesRequirement {
694785 subject,
695786 outlived_free_region: static_r,
696787 blame_span,
697788 category: ConstraintCategory :: Boring ,
698- } ) ;
789+ } ] ) ;
699790
700791 // we can return here -- the code below might push add'l constraints
701792 // but they would all be weaker than this one.
702793 return true ;
703794 }
704795
705- // For each region outlived by lower_bound find a non-local,
706- // universal region (it may be the same region) and add it to
707- // `ClosureOutlivesRequirement`.
708- let mut found_outlived_universal_region = false ;
709- for ur in self . scc_values . universal_regions_outlived_by ( r_scc) {
710- found_outlived_universal_region = true ;
796+ let universal_regions: Vec < _ > =
797+ self . scc_values . universal_regions_outlived_by ( r_scc) . collect ( ) ;
798+ debug ! ( ?universal_regions) ;
799+
800+ // Filter to only the "minimal" universal regions:
801+ // Drop any region `a` that strictly outlives another region `b`.
802+ let minimal_universal_regions: Vec < _ > = universal_regions
803+ . iter ( )
804+ . copied ( )
805+ . filter ( |& a| {
806+ !universal_regions. iter ( ) . copied ( ) . any ( |b| {
807+ !self . universal_region_relations . outlives ( a, b)
808+ && self . universal_region_relations . outlives ( b, a)
809+ } )
810+ } )
811+ . collect ( ) ;
812+
813+ assert ! (
814+ !minimal_universal_regions. is_empty( ) ,
815+ "There should always be at least 1 minimal region"
816+ ) ;
817+
818+ for ur in minimal_universal_regions {
711819 debug ! ( "universal_region_outlived_by ur={:?}" , ur) ;
712820 let non_local_ub = self . universal_region_relations . non_local_upper_bounds ( ur) ;
713821 debug ! ( ?non_local_ub) ;
@@ -716,6 +824,7 @@ impl<'tcx> RegionInferenceContext<'tcx> {
716824 // and `'3: '1` we only need to prove that T: '2 *or* T: '3, but to
717825 // avoid potential non-determinism we approximate this by requiring
718826 // T: '1 and T: '2.
827+ let mut or_requirements = Vec :: with_capacity ( non_local_ub. len ( ) ) ;
719828 for upper_bound in non_local_ub {
720829 debug_assert ! ( self . universal_regions( ) . is_universal_region( upper_bound) ) ;
721830 debug_assert ! ( !self . universal_regions( ) . is_local_free_region( upper_bound) ) ;
@@ -727,14 +836,10 @@ impl<'tcx> RegionInferenceContext<'tcx> {
727836 category : ConstraintCategory :: Boring ,
728837 } ;
729838 debug ! ( ?requirement, "adding closure requirement" ) ;
730- propagated_outlives_requirements . push ( requirement) ;
839+ or_requirements . push ( requirement) ;
731840 }
841+ propagated_outlives_requirements. push ( or_requirements) ;
732842 }
733- // If we succeed to promote the subject, i.e. it only contains non-local regions,
734- // and fail to prove the type test inside of the closure, the `lower_bound` has to
735- // also be at least as large as some universal region, as the type test is otherwise
736- // trivial.
737- assert ! ( found_outlived_universal_region) ;
738843 true
739844 }
740845
0 commit comments