Remove contraction from region inference

src/librustc/middle/def_id.rs

@@ -61,12 +61,16 @@ impl fmt::Debug for DefId {
         // Unfortunately, there seems to be no way to attempt to print
         // a path for a def-id, so I'll just make a best effort for now
         // and otherwise fallback to just printing the crate/node pair
-        try!(ty::tls::with_opt(|opt_tcx| {
-            if let Some(tcx) = opt_tcx {
-                try!(write!(f, " => {}", tcx.item_path_str(*self)));
-            }
-            Ok(())
-        }));
+        if self.is_local() { // (1)
+            // (1) side-step fact that not all external things have paths at
+            // the moment, such as type parameters
+            try!(ty::tls::with_opt(|opt_tcx| {
+                if let Some(tcx) = opt_tcx {
+                    try!(write!(f, " => {}", tcx.item_path_str(*self)));
+                }
+                Ok(())
+            }));
+        }
 
         write!(f, " }}")
     }

src/librustc/middle/infer/error_reporting.rs

@@ -65,7 +65,6 @@ use super::ValuePairs;
 use super::region_inference::RegionResolutionError;
 use super::region_inference::ConcreteFailure;
 use super::region_inference::SubSupConflict;
-use super::region_inference::SupSupConflict;
 use super::region_inference::GenericBoundFailure;
 use super::region_inference::GenericKind;
 use super::region_inference::ProcessedErrors;
@@ -258,13 +257,6 @@ pub trait ErrorReporting<'tcx> {
                                sup_origin: SubregionOrigin<'tcx>,
                                sup_region: Region);
 
-    fn report_sup_sup_conflict(&self,
-                               var_origin: RegionVariableOrigin,
-                               origin1: SubregionOrigin<'tcx>,
-                               region1: Region,
-                               origin2: SubregionOrigin<'tcx>,
-                               region2: Region);
-
     fn report_processed_errors(&self,
                                var_origin: &[RegionVariableOrigin],
                                trace_origin: &[(TypeTrace<'tcx>, TypeError<'tcx>)],
@@ -313,14 +305,6 @@ impl<'a, 'tcx> ErrorReporting<'tcx> for InferCtxt<'a, 'tcx> {
                                                  sup_origin, sup_r);
                 }
 
-                SupSupConflict(var_origin,
-                               origin1, r1,
-                               origin2, r2) => {
-                    self.report_sup_sup_conflict(var_origin,
-                                                 origin1, r1,
-                                                 origin2, r2);
-                }
-
                 ProcessedErrors(ref var_origins,
                                 ref trace_origins,
                                 ref same_regions) => {
@@ -376,7 +360,6 @@ impl<'a, 'tcx> ErrorReporting<'tcx> for InferCtxt<'a, 'tcx> {
                         None => processed_errors.push((*error).clone()),
                     }
                 }
-                SupSupConflict(..) => processed_errors.push((*error).clone()),
                 _ => ()  // This shouldn't happen
             }
         }
@@ -930,29 +913,6 @@ impl<'a, 'tcx> ErrorReporting<'tcx> for InferCtxt<'a, 'tcx> {
         self.note_region_origin(&sub_origin);
     }
 
-    fn report_sup_sup_conflict(&self,
-                               var_origin: RegionVariableOrigin,
-                               origin1: SubregionOrigin<'tcx>,
-                               region1: Region,
-                               origin2: SubregionOrigin<'tcx>,
-                               region2: Region) {
-        self.report_inference_failure(var_origin);
-
-        self.tcx.note_and_explain_region(
-            "first, the lifetime must be contained by ",
-            region1,
-            "...");
-
-        self.note_region_origin(&origin1);
-
-        self.tcx.note_and_explain_region(
-            "but, the lifetime must also be contained by ",
-            region2,
-            "...");
-
-        self.note_region_origin(&origin2);
-    }
-
     fn report_processed_errors(&self,
                                var_origins: &[RegionVariableOrigin],
                                trace_origins: &[(TypeTrace<'tcx>, TypeError<'tcx>)],

src/librustc/middle/infer/region_inference/README.md

@@ -2,13 +2,12 @@ Region inference
 
 # Terminology
 
-Note that we use the terms region and lifetime interchangeably,
-though the term `lifetime` is preferred.
+Note that we use the terms region and lifetime interchangeably.
 
 # Introduction
 
 Region inference uses a somewhat more involved algorithm than type
-inference.  It is not the most efficient thing ever written though it
+inference. It is not the most efficient thing ever written though it
 seems to work well enough in practice (famous last words).  The reason
 that we use a different algorithm is because, unlike with types, it is
 impractical to hand-annotate with regions (in some cases, there aren't
@@ -25,22 +24,42 @@ once.
 
 The constraints are always of one of three possible forms:
 
-- ConstrainVarSubVar(R_i, R_j) states that region variable R_i
-  must be a subregion of R_j
-- ConstrainRegSubVar(R, R_i) states that the concrete region R
-  (which must not be a variable) must be a subregion of the variable R_i
-- ConstrainVarSubReg(R_i, R) is the inverse
+- `ConstrainVarSubVar(Ri, Rj)` states that region variable Ri must be
+  a subregion of Rj
+- `ConstrainRegSubVar(R, Ri)` states that the concrete region R (which
+  must not be a variable) must be a subregion of the variable Ri
+- `ConstrainVarSubReg(Ri, R)` states the variable Ri shoudl be less
+  than the concrete region R. This is kind of deprecated and ought to
+  be replaced with a verify (they essentially play the same role).
+
+In addition to constraints, we also gather up a set of "verifys"
+(what, you don't think Verify is a noun? Get used to it my
+friend!). These represent relations that must hold but which don't
+influence inference proper. These take the form of:
+
+- `VerifyRegSubReg(Ri, Rj)` indicates that Ri <= Rj must hold,
+  where Rj is not an inference variable (and Ri may or may not contain
+  one). This doesn't influence inference because we will already have
+  inferred Ri to be as small as possible, so then we just test whether
+  that result was less than Rj or not.
+- `VerifyGenericBound(R, Vb)` is a more complex expression which tests
+  that the region R must satisfy the bound `Vb`. The bounds themselves
+  may have structure like "must outlive one of the following regions"
+  or "must outlive ALL of the following regions. These bounds arise
+  from constraints like `T: 'a` -- if we know that `T: 'b` and `T: 'c`
+  (say, from where clauses), then we can conclude that `T: 'a` if `'b:
+  'a` *or* `'c: 'a`.
 
 # Building up the constraints
 
 Variables and constraints are created using the following methods:
 
 - `new_region_var()` creates a new, unconstrained region variable;
-- `make_subregion(R_i, R_j)` states that R_i is a subregion of R_j
-- `lub_regions(R_i, R_j) -> R_k` returns a region R_k which is
-  the smallest region that is greater than both R_i and R_j
-- `glb_regions(R_i, R_j) -> R_k` returns a region R_k which is
-  the greatest region that is smaller than both R_i and R_j
+- `make_subregion(Ri, Rj)` states that Ri is a subregion of Rj
+- `lub_regions(Ri, Rj) -> Rk` returns a region Rk which is
+  the smallest region that is greater than both Ri and Rj
+- `glb_regions(Ri, Rj) -> Rk` returns a region Rk which is
+  the greatest region that is smaller than both Ri and Rj
 
 The actual region resolution algorithm is not entirely
 obvious, though it is also not overly complex.
@@ -54,14 +73,6 @@ Alternatively, you can call `commit()` which ends all snapshots.
 Snapshots can be recursive---so you can start a snapshot when another
 is in progress, but only the root snapshot can "commit".
 
-# Resolving constraints
-
-The constraint resolution algorithm is not super complex but also not
-entirely obvious.  Here I describe the problem somewhat abstractly,
-then describe how the current code works.  There may be other, smarter
-ways of doing this with which I am unfamiliar and can't be bothered to
-research at the moment. - NDM
-
 ## The problem
 
 Basically our input is a directed graph where nodes can be divided
@@ -83,31 +94,20 @@ Before resolution begins, we build up the constraints in a hashmap
 that maps `Constraint` keys to spans.  During resolution, we construct
 the actual `Graph` structure that we describe here.
 
-## Our current algorithm
-
-We divide region variables into two groups: Expanding and Contracting.
-Expanding region variables are those that have a concrete region
-predecessor (direct or indirect).  Contracting region variables are
-all others.
-
-We first resolve the values of Expanding region variables and then
-process Contracting ones.  We currently use an iterative, fixed-point
-procedure (but read on, I believe this could be replaced with a linear
-walk).  Basically we iterate over the edges in the graph, ensuring
-that, if the source of the edge has a value, then this value is a
-subregion of the target value.  If the target does not yet have a
-value, it takes the value from the source.  If the target already had
-a value, then the resulting value is Least Upper Bound of the old and
-new values. When we are done, each Expanding node will have the
-smallest region that it could possibly have and still satisfy the
-constraints.
-
-We next process the Contracting nodes.  Here we again iterate over the
-edges, only this time we move values from target to source (if the
-source is a Contracting node).  For each contracting node, we compute
-its value as the GLB of all its successors.  Basically contracting
-nodes ensure that there is overlap between their successors; we will
-ultimately infer the largest overlap possible.
+## Computing the values for region variables
+
+The algorithm is a simple dataflow algorithm. Each region variable
+begins as empty. We iterate over the constraints, and for each constraint
+we grow the relevant region variable to be as big as it must be to meet all the
+constraints. This means the region variables can grow to be `'static` if
+necessary.
+
+## Verification
+
+After all constraints are fully propoagated, we do a "verification"
+step where we walk over the verify bounds and check that they are
+satisfied. These bounds represent the "maximal" values that a region
+variable can take on, basically.
 
 # The Region Hierarchy