Skip to main content

hir_ty/next_solver/infer/region_constraints/
mod.rs

1//! See `README.md`.
2
3use std::ops::Range;
4use std::{cmp, fmt, mem};
5
6use ena::undo_log::{Rollback, UndoLogs};
7use ena::unify as ut;
8use rustc_hash::FxHashMap;
9use rustc_index::IndexVec;
10use rustc_type_ir::inherent::IntoKind;
11use rustc_type_ir::{RegionKind, RegionVid, UniverseIndex};
12use tracing::{debug, instrument};
13
14use self::CombineMapType::*;
15use self::UndoLog::*;
16use super::MemberConstraint;
17use super::unify_key::RegionVidKey;
18use crate::next_solver::infer::unify_key::RegionVariableValue;
19use crate::next_solver::{AliasTy, Binder, DbInterner, ParamTy, PlaceholderType, Region, Ty};
20use crate::{
21    Span,
22    next_solver::infer::snapshot::undo_log::{InferCtxtUndoLogs, Snapshot},
23};
24
25#[derive(Debug, Clone, Default)]
26pub struct RegionConstraintStorage<'db> {
27    /// For each `RegionVid`, the corresponding `RegionVariableOrigin`.
28    pub(super) var_infos: IndexVec<RegionVid, RegionVariableInfo>,
29
30    pub(super) data: RegionConstraintData<'db>,
31
32    /// For a given pair of regions (R1, R2), maps to a region R3 that
33    /// is designated as their LUB (edges R1 <= R3 and R2 <= R3
34    /// exist). This prevents us from making many such regions.
35    lubs: CombineMap<'db>,
36
37    /// For a given pair of regions (R1, R2), maps to a region R3 that
38    /// is designated as their GLB (edges R3 <= R1 and R3 <= R2
39    /// exist). This prevents us from making many such regions.
40    glbs: CombineMap<'db>,
41
42    /// When we add a R1 == R2 constraint, we currently add (a) edges
43    /// R1 <= R2 and R2 <= R1 and (b) we unify the two regions in this
44    /// table. You can then call `opportunistic_resolve_var` early
45    /// which will map R1 and R2 to some common region (i.e., either
46    /// R1 or R2). This is important when fulfillment, dropck and other such
47    /// code is iterating to a fixed point, because otherwise we sometimes
48    /// would wind up with a fresh stream of region variables that have been
49    /// equated but appear distinct.
50    pub(super) unification_table: ut::UnificationTableStorage<RegionVidKey<'db>>,
51
52    /// a flag set to true when we perform any unifications; this is used
53    /// to micro-optimize `take_and_reset_data`
54    any_unifications: bool,
55}
56
57pub struct RegionConstraintCollector<'db, 'a> {
58    storage: &'a mut RegionConstraintStorage<'db>,
59    undo_log: &'a mut InferCtxtUndoLogs<'db>,
60}
61
62pub type VarInfos = IndexVec<RegionVid, RegionVariableInfo>;
63
64/// The full set of region constraints gathered up by the collector.
65/// Describes constraints between the region variables and other
66/// regions, as well as other conditions that must be verified, or
67/// assumptions that can be made.
68#[derive(Debug, Default, Clone)]
69pub struct RegionConstraintData<'db> {
70    /// Constraints of the form `A <= B`, where either `A` or `B` can
71    /// be a region variable (or neither, as it happens).
72    pub constraints: Vec<Constraint<'db>>,
73
74    /// Constraints of the form `R0 member of [R1, ..., Rn]`, meaning that
75    /// `R0` must be equal to one of the regions `R1..Rn`. These occur
76    /// with `impl Trait` quite frequently.
77    pub member_constraints: Vec<MemberConstraint<'db>>,
78
79    /// A "verify" is something that we need to verify after inference
80    /// is done, but which does not directly affect inference in any
81    /// way.
82    ///
83    /// An example is a `A <= B` where neither `A` nor `B` are
84    /// inference variables.
85    pub verifys: Vec<Verify<'db>>,
86}
87
88/// Represents a constraint that influences the inference process.
89#[derive(Clone, PartialEq, Eq, Debug, Hash)]
90pub enum Constraint<'db> {
91    /// A region variable is a subregion of another.
92    VarSubVar(RegionVid, RegionVid),
93
94    /// A concrete region is a subregion of region variable.
95    RegSubVar(Region<'db>, RegionVid),
96
97    /// A region variable is a subregion of a concrete region. This does not
98    /// directly affect inference, but instead is checked after
99    /// inference is complete.
100    VarSubReg(RegionVid, Region<'db>),
101
102    /// A constraint where neither side is a variable. This does not
103    /// directly affect inference, but instead is checked after
104    /// inference is complete.
105    RegSubReg(Region<'db>, Region<'db>),
106}
107
108impl<'db> Constraint<'db> {
109    pub fn involves_placeholders(&self) -> bool {
110        match self {
111            Constraint::VarSubVar(_, _) => false,
112            Constraint::VarSubReg(_, r) | Constraint::RegSubVar(r, _) => r.is_placeholder(),
113            Constraint::RegSubReg(r, s) => r.is_placeholder() || s.is_placeholder(),
114        }
115    }
116}
117
118#[derive(Debug, Clone)]
119pub struct Verify<'db> {
120    pub kind: GenericKind<'db>,
121    pub region: Region<'db>,
122    pub bound: VerifyBound<'db>,
123}
124
125#[derive(Clone, PartialEq, Eq, Hash)]
126pub enum GenericKind<'db> {
127    Param(ParamTy),
128    Placeholder(PlaceholderType<'db>),
129    Alias(AliasTy<'db>),
130}
131
132/// Describes the things that some `GenericKind` value `G` is known to
133/// outlive. Each variant of `VerifyBound` can be thought of as a
134/// function:
135/// ```ignore (pseudo-rust)
136/// fn(min: Region) -> bool { .. }
137/// ```
138/// where `true` means that the region `min` meets that `G: min`.
139/// (False means nothing.)
140///
141/// So, for example, if we have the type `T` and we have in scope that
142/// `T: 'a` and `T: 'b`, then the verify bound might be:
143/// ```ignore (pseudo-rust)
144/// fn(min: Region) -> bool {
145///    ('a: min) || ('b: min)
146/// }
147/// ```
148/// This is described with an `AnyRegion('a, 'b)` node.
149#[derive(Debug, Clone)]
150pub enum VerifyBound<'db> {
151    /// See [`VerifyIfEq`] docs
152    IfEq(Binder<'db, VerifyIfEq<'db>>),
153
154    /// Given a region `R`, expands to the function:
155    ///
156    /// ```ignore (pseudo-rust)
157    /// fn(min) -> bool {
158    ///     R: min
159    /// }
160    /// ```
161    ///
162    /// This is used when we can establish that `G: R` -- therefore,
163    /// if `R: min`, then by transitivity `G: min`.
164    OutlivedBy(Region<'db>),
165
166    /// Given a region `R`, true if it is `'empty`.
167    IsEmpty,
168
169    /// Given a set of bounds `B`, expands to the function:
170    ///
171    /// ```ignore (pseudo-rust)
172    /// fn(min) -> bool {
173    ///     exists (b in B) { b(min) }
174    /// }
175    /// ```
176    ///
177    /// In other words, if we meet some bound in `B`, that suffices.
178    /// This is used when all the bounds in `B` are known to apply to `G`.
179    AnyBound(Vec<VerifyBound<'db>>),
180
181    /// Given a set of bounds `B`, expands to the function:
182    ///
183    /// ```ignore (pseudo-rust)
184    /// fn(min) -> bool {
185    ///     forall (b in B) { b(min) }
186    /// }
187    /// ```
188    ///
189    /// In other words, if we meet *all* bounds in `B`, that suffices.
190    /// This is used when *some* bound in `B` is known to suffice, but
191    /// we don't know which.
192    AllBounds(Vec<VerifyBound<'db>>),
193}
194
195/// This is a "conditional bound" that checks the result of inference
196/// and supplies a bound if it ended up being relevant. It's used in situations
197/// like this:
198///
199/// ```rust,ignore (pseudo-Rust)
200/// fn foo<'a, 'b, T: SomeTrait<'a>>
201/// where
202///    <T as SomeTrait<'a>>::Item: 'b
203/// ```
204///
205/// If we have an obligation like `<T as SomeTrait<'?x>>::Item: 'c`, then
206/// we don't know yet whether it suffices to show that `'b: 'c`. If `'?x` winds
207/// up being equal to `'a`, then the where-clauses on function applies, and
208/// in that case we can show `'b: 'c`. But if `'?x` winds up being something
209/// else, the bound isn't relevant.
210///
211/// In the [`VerifyBound`], this struct is enclosed in `Binder` to account
212/// for cases like
213///
214/// ```rust,ignore (pseudo-Rust)
215/// where for<'a> <T as SomeTrait<'a>::Item: 'a
216/// ```
217///
218/// The idea is that we have to find some instantiation of `'a` that can
219/// make `<T as SomeTrait<'a>>::Item` equal to the final value of `G`,
220/// the generic we are checking.
221///
222/// ```ignore (pseudo-rust)
223/// fn(min) -> bool {
224///     exists<'a> {
225///         if G == K {
226///             B(min)
227///         } else {
228///             false
229///         }
230///     }
231/// }
232/// ```
233#[derive(Debug, Clone)]
234pub struct VerifyIfEq<'db> {
235    /// Type which must match the generic `G`
236    pub ty: Ty<'db>,
237
238    /// Bound that applies if `ty` is equal.
239    pub bound: Region<'db>,
240}
241
242#[derive(Debug, Clone, PartialEq, Eq, Hash)]
243pub(crate) struct TwoRegions<'db> {
244    a: Region<'db>,
245    b: Region<'db>,
246}
247
248#[derive(Clone, PartialEq)]
249pub(crate) enum UndoLog<'db> {
250    /// We added `RegionVid`.
251    AddVar(RegionVid),
252
253    /// We added the given `constraint`.
254    AddConstraint(usize),
255
256    /// We added the given `verify`.
257    #[expect(dead_code, reason = "this is used in rustc")]
258    AddVerify(usize),
259
260    /// We added a GLB/LUB "combination variable".
261    AddCombination(CombineMapType, TwoRegions<'db>),
262}
263
264#[derive(Clone, PartialEq)]
265pub(crate) enum CombineMapType {
266    Lub,
267    Glb,
268}
269
270type CombineMap<'db> = FxHashMap<TwoRegions<'db>, RegionVid>;
271
272#[derive(Debug, Clone)]
273pub struct RegionVariableInfo {
274    // FIXME: This is only necessary for `fn take_and_reset_data` and
275    // `lexical_region_resolve`. We should rework `lexical_region_resolve`
276    // in the near/medium future anyways and could move the unverse info
277    // for `fn take_and_reset_data` into a separate table which is
278    // only populated when needed.
279    //
280    // For both of these cases it is fine that this can diverge from the
281    // actual universe of the variable, which is directly stored in the
282    // unification table for unknown region variables. At some point we could
283    // stop emitting bidirectional outlives constraints if equate succeeds.
284    // This would be currently unsound as it would cause us to drop the universe
285    // changes in `lexical_region_resolve`.
286    pub universe: UniverseIndex,
287    pub span: Span,
288}
289
290pub(crate) struct RegionSnapshot {
291    any_unifications: bool,
292}
293
294impl<'db> RegionConstraintStorage<'db> {
295    #[inline]
296    pub(crate) fn with_log<'a>(
297        &'a mut self,
298        undo_log: &'a mut InferCtxtUndoLogs<'db>,
299    ) -> RegionConstraintCollector<'db, 'a> {
300        RegionConstraintCollector { storage: self, undo_log }
301    }
302}
303
304impl<'db> RegionConstraintCollector<'db, '_> {
305    pub fn num_region_vars(&self) -> usize {
306        self.storage.var_infos.len()
307    }
308
309    pub fn region_constraint_data(&self) -> &RegionConstraintData<'db> {
310        &self.storage.data
311    }
312
313    /// Takes (and clears) the current set of constraints. Note that
314    /// the set of variables remains intact, but all relationships
315    /// between them are reset. This is used during NLL checking to
316    /// grab the set of constraints that arose from a particular
317    /// operation.
318    ///
319    /// We don't want to leak relationships between variables between
320    /// points because just because (say) `r1 == r2` was true at some
321    /// point P in the graph doesn't imply that it will be true at
322    /// some other point Q, in NLL.
323    ///
324    /// Not legal during a snapshot.
325    pub fn take_and_reset_data(&mut self) -> RegionConstraintData<'db> {
326        assert!(!UndoLogs::<UndoLog<'db>>::in_snapshot(&self.undo_log));
327
328        // If you add a new field to `RegionConstraintCollector`, you
329        // should think carefully about whether it needs to be cleared
330        // or updated in some way.
331        let RegionConstraintStorage {
332            var_infos: _,
333            data,
334            lubs,
335            glbs,
336            unification_table: _,
337            any_unifications,
338        } = self.storage;
339
340        // Clear the tables of (lubs, glbs), so that we will create
341        // fresh regions if we do a LUB operation. As it happens,
342        // LUB/GLB are not performed by the MIR type-checker, which is
343        // the one that uses this method, but it's good to be correct.
344        lubs.clear();
345        glbs.clear();
346
347        let data = mem::take(data);
348
349        // Clear all unifications and recreate the variables a "now
350        // un-unified" state. Note that when we unify `a` and `b`, we
351        // also insert `a <= b` and a `b <= a` edges, so the
352        // `RegionConstraintData` contains the relationship here.
353        if *any_unifications {
354            *any_unifications = false;
355            // Manually inlined `self.unification_table_mut()` as `self` is used in the closure.
356            ut::UnificationTable::with_log(&mut self.storage.unification_table, &mut self.undo_log)
357                .reset_unifications(|key| {
358                    let var_info = &self.storage.var_infos[key.vid];
359                    RegionVariableValue::Unknown {
360                        universe: var_info.universe,
361                        span: var_info.span,
362                    }
363                });
364        }
365
366        data
367    }
368
369    pub fn data(&self) -> &RegionConstraintData<'db> {
370        &self.storage.data
371    }
372
373    pub(super) fn start_snapshot(&self) -> RegionSnapshot {
374        debug!("RegionConstraintCollector: start_snapshot");
375        RegionSnapshot { any_unifications: self.storage.any_unifications }
376    }
377
378    pub(super) fn rollback_to(&mut self, snapshot: RegionSnapshot) {
379        debug!("RegionConstraintCollector: rollback_to({:?})", snapshot);
380        self.storage.any_unifications = snapshot.any_unifications;
381    }
382
383    pub(super) fn new_region_var(&mut self, universe: UniverseIndex, span: Span) -> RegionVid {
384        let vid = self.storage.var_infos.push(RegionVariableInfo { universe, span });
385
386        let u_vid =
387            self.unification_table_mut().new_key(RegionVariableValue::Unknown { universe, span });
388        assert_eq!(vid, u_vid.vid);
389        self.undo_log.push(AddVar(vid));
390        debug!("created new region variable {:?} in {:?}", vid, universe);
391        vid
392    }
393
394    fn add_constraint(&mut self, constraint: Constraint<'db>) {
395        // cannot add constraints once regions are resolved
396        debug!("RegionConstraintCollector: add_constraint({:?})", constraint);
397
398        let index = self.storage.data.constraints.len();
399        self.storage.data.constraints.push(constraint);
400        self.undo_log.push(AddConstraint(index));
401    }
402
403    pub(super) fn make_eqregion(&mut self, a: Region<'db>, b: Region<'db>) {
404        if a != b {
405            // Eventually, it would be nice to add direct support for
406            // equating regions.
407            self.make_subregion(a, b);
408            self.make_subregion(b, a);
409
410            match (a.kind(), b.kind()) {
411                (RegionKind::ReVar(a), RegionKind::ReVar(b)) => {
412                    debug!("make_eqregion: unifying {:?} with {:?}", a, b);
413                    if self.unification_table_mut().unify_var_var(a, b).is_ok() {
414                        self.storage.any_unifications = true;
415                    }
416                }
417                (RegionKind::ReVar(vid), _) => {
418                    debug!("make_eqregion: unifying {:?} with {:?}", vid, b);
419                    if self
420                        .unification_table_mut()
421                        .unify_var_value(vid, RegionVariableValue::Known { value: b, span: None })
422                        .is_ok()
423                    {
424                        self.storage.any_unifications = true;
425                    };
426                }
427                (_, RegionKind::ReVar(vid)) => {
428                    debug!("make_eqregion: unifying {:?} with {:?}", a, vid);
429                    if self
430                        .unification_table_mut()
431                        .unify_var_value(vid, RegionVariableValue::Known { value: a, span: None })
432                        .is_ok()
433                    {
434                        self.storage.any_unifications = true;
435                    };
436                }
437                (_, _) => {}
438            }
439        }
440    }
441
442    #[instrument(skip(self), level = "debug")]
443    pub(super) fn make_subregion(&mut self, sub: Region<'db>, sup: Region<'db>) {
444        // cannot add constraints once regions are resolved
445
446        match (sub.kind(), sup.kind()) {
447            (RegionKind::ReBound(..), _) | (_, RegionKind::ReBound(..)) => {
448                panic!("cannot relate bound region: {sub:?} <= {sup:?}");
449            }
450            (_, RegionKind::ReStatic) => {
451                // all regions are subregions of static, so we can ignore this
452            }
453            (RegionKind::ReVar(sub_id), RegionKind::ReVar(sup_id)) => {
454                self.add_constraint(Constraint::VarSubVar(sub_id, sup_id));
455            }
456            (_, RegionKind::ReVar(sup_id)) => {
457                self.add_constraint(Constraint::RegSubVar(sub, sup_id));
458            }
459            (RegionKind::ReVar(sub_id), _) => {
460                self.add_constraint(Constraint::VarSubReg(sub_id, sup));
461            }
462            _ => {
463                self.add_constraint(Constraint::RegSubReg(sub, sup));
464            }
465        }
466    }
467
468    pub(super) fn lub_regions(
469        &mut self,
470        db: DbInterner<'db>,
471        origin: Span,
472        a: Region<'db>,
473        b: Region<'db>,
474    ) -> Region<'db> {
475        // cannot add constraints once regions are resolved
476        debug!("RegionConstraintCollector: lub_regions({:?}, {:?})", a, b);
477        #[expect(clippy::if_same_then_else)]
478        if a.is_static() || b.is_static() {
479            a // nothing lives longer than static
480        } else if a == b {
481            a // LUB(a,a) = a
482        } else {
483            self.combine_vars(db, Lub, a, b, origin)
484        }
485    }
486
487    pub(super) fn glb_regions(
488        &mut self,
489        db: DbInterner<'db>,
490        origin: Span,
491        a: Region<'db>,
492        b: Region<'db>,
493    ) -> Region<'db> {
494        // cannot add constraints once regions are resolved
495        debug!("RegionConstraintCollector: glb_regions({:?}, {:?})", a, b);
496        #[expect(clippy::if_same_then_else)]
497        if a.is_static() {
498            b // static lives longer than everything else
499        } else if b.is_static() {
500            a // static lives longer than everything else
501        } else if a == b {
502            a // GLB(a,a) = a
503        } else {
504            self.combine_vars(db, Glb, a, b, origin)
505        }
506    }
507
508    /// Resolves a region var to its value in the unification table, if it exists.
509    /// Otherwise, it is resolved to the root `ReVar` in the table.
510    pub fn opportunistic_resolve_var(
511        &mut self,
512        cx: DbInterner<'db>,
513        vid: RegionVid,
514    ) -> Region<'db> {
515        let mut ut = self.unification_table_mut();
516        let root_vid = ut.find(vid).vid;
517        match ut.probe_value(root_vid) {
518            RegionVariableValue::Known { value, .. } => value,
519            RegionVariableValue::Unknown { .. } => Region::new_var(cx, root_vid),
520        }
521    }
522
523    pub fn probe_value(&mut self, vid: RegionVid) -> Result<Region<'db>, UniverseIndex> {
524        match self.unification_table_mut().probe_value(vid) {
525            RegionVariableValue::Known { value, .. } => Ok(value),
526            RegionVariableValue::Unknown { universe, .. } => Err(universe),
527        }
528    }
529
530    fn combine_map(&mut self, t: CombineMapType) -> &mut CombineMap<'db> {
531        match t {
532            Glb => &mut self.storage.glbs,
533            Lub => &mut self.storage.lubs,
534        }
535    }
536
537    fn combine_vars(
538        &mut self,
539        cx: DbInterner<'db>,
540        t: CombineMapType,
541        a: Region<'db>,
542        b: Region<'db>,
543        origin: Span,
544    ) -> Region<'db> {
545        let vars = TwoRegions { a, b };
546        if let Some(c) = self.combine_map(t.clone()).get(&vars) {
547            return Region::new_var(cx, *c);
548        }
549        let a_universe = self.universe(a);
550        let b_universe = self.universe(b);
551        let c_universe = cmp::max(a_universe, b_universe);
552        let c = self.new_region_var(c_universe, origin);
553        self.combine_map(t.clone()).insert(vars.clone(), c);
554        self.undo_log.push(AddCombination(t.clone(), vars));
555        let new_r = Region::new_var(cx, c);
556        for old_r in [a, b] {
557            match t {
558                Glb => self.make_subregion(new_r, old_r),
559                Lub => self.make_subregion(old_r, new_r),
560            }
561        }
562        debug!("combine_vars() c={:?}", c);
563        new_r
564    }
565
566    pub fn universe(&mut self, region: Region<'db>) -> UniverseIndex {
567        match region.kind() {
568            RegionKind::ReStatic
569            | RegionKind::ReErased
570            | RegionKind::ReLateParam(..)
571            | RegionKind::ReEarlyParam(..)
572            | RegionKind::ReError(_) => UniverseIndex::ROOT,
573            RegionKind::RePlaceholder(placeholder) => placeholder.universe,
574            RegionKind::ReVar(vid) => match self.probe_value(vid) {
575                Ok(value) => self.universe(value),
576                Err(universe) => universe,
577            },
578            RegionKind::ReBound(..) => panic!("universe(): encountered bound region {region:?}"),
579        }
580    }
581
582    pub fn vars_since_snapshot(&self, value_count: usize) -> (Range<RegionVid>, Vec<Span>) {
583        let range =
584            RegionVid::from(value_count)..RegionVid::from(self.storage.unification_table.len());
585        (
586            range.clone(),
587            (range.start.as_usize()..range.end.as_usize())
588                .map(|index| self.storage.var_infos[RegionVid::from_usize(index)].span)
589                .collect(),
590        )
591    }
592
593    /// See `InferCtxt::region_constraints_added_in_snapshot`.
594    pub fn region_constraints_added_in_snapshot(&self, mark: &Snapshot) -> bool {
595        self.undo_log
596            .region_constraints_in_snapshot(mark)
597            .any(|elt| matches!(elt, AddConstraint(_)))
598    }
599
600    #[inline]
601    fn unification_table_mut(&mut self) -> super::UnificationTable<'_, 'db, RegionVidKey<'db>> {
602        ut::UnificationTable::with_log(&mut self.storage.unification_table, self.undo_log)
603    }
604}
605
606impl fmt::Debug for RegionSnapshot {
607    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
608        write!(f, "RegionSnapshot")
609    }
610}
611
612impl<'db> fmt::Debug for GenericKind<'db> {
613    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
614        match *self {
615            GenericKind::Param(ref p) => write!(f, "{p:?}"),
616            GenericKind::Placeholder(ref p) => write!(f, "{p:?}"),
617            GenericKind::Alias(ref p) => write!(f, "{p:?}"),
618        }
619    }
620}
621
622impl<'db> fmt::Display for GenericKind<'db> {
623    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
624        match *self {
625            GenericKind::Param(ref p) => write!(f, "{p:?}"),
626            GenericKind::Placeholder(ref p) => write!(f, "{p:?}"),
627            GenericKind::Alias(ref p) => write!(f, "{p}"),
628        }
629    }
630}
631
632impl<'db> GenericKind<'db> {
633    pub fn to_ty(&self, interner: DbInterner<'db>) -> Ty<'db> {
634        match *self {
635            GenericKind::Param(ref p) => (*p).to_ty(interner),
636            GenericKind::Placeholder(ref p) => Ty::new_placeholder(interner, *p),
637            GenericKind::Alias(ref p) => (*p).to_ty(interner),
638        }
639    }
640}
641
642impl<'db> VerifyBound<'db> {
643    pub fn must_hold(&self) -> bool {
644        match self {
645            VerifyBound::IfEq(..) => false,
646            VerifyBound::OutlivedBy(re) => re.is_static(),
647            VerifyBound::IsEmpty => false,
648            VerifyBound::AnyBound(bs) => bs.iter().any(|b| b.must_hold()),
649            VerifyBound::AllBounds(bs) => bs.iter().all(|b| b.must_hold()),
650        }
651    }
652
653    pub fn cannot_hold(&self) -> bool {
654        match self {
655            VerifyBound::IfEq(..) => false,
656            VerifyBound::IsEmpty => false,
657            VerifyBound::OutlivedBy(_) => false,
658            VerifyBound::AnyBound(bs) => bs.iter().all(|b| b.cannot_hold()),
659            VerifyBound::AllBounds(bs) => bs.iter().any(|b| b.cannot_hold()),
660        }
661    }
662
663    pub fn or(self, vb: VerifyBound<'db>) -> VerifyBound<'db> {
664        if self.must_hold() || vb.cannot_hold() {
665            self
666        } else if self.cannot_hold() || vb.must_hold() {
667            vb
668        } else {
669            VerifyBound::AnyBound(vec![self, vb])
670        }
671    }
672}
673
674impl<'db> RegionConstraintData<'db> {
675    /// Returns `true` if this region constraint data contains no constraints, and `false`
676    /// otherwise.
677    pub fn is_empty(&self) -> bool {
678        let RegionConstraintData { constraints, member_constraints, verifys } = self;
679        constraints.is_empty() && member_constraints.is_empty() && verifys.is_empty()
680    }
681}
682
683impl<'db> Rollback<UndoLog<'db>> for RegionConstraintStorage<'db> {
684    fn reverse(&mut self, undo: UndoLog<'db>) {
685        match undo {
686            AddVar(vid) => {
687                self.var_infos.pop().unwrap();
688                assert_eq!(self.var_infos.len(), vid.index());
689            }
690            AddConstraint(index) => {
691                self.data.constraints.pop().unwrap();
692                assert_eq!(self.data.constraints.len(), index);
693            }
694            AddVerify(index) => {
695                self.data.verifys.pop();
696                assert_eq!(self.data.verifys.len(), index);
697            }
698            AddCombination(Glb, ref regions) => {
699                self.glbs.remove(regions);
700            }
701            AddCombination(Lub, ref regions) => {
702                self.lubs.remove(regions);
703            }
704        }
705    }
706}