sgrif-plan-skolemized-removal.md

This is the rough implementation plan:

pick 9ae5db20d2 introduce Universe struct

We want this. =)

pick 1da0b70c57 introduce UniverseIndex into ParamEnv

Instead of adding a universe to the ParamEnv, the plan is now to add this field to the InferenceCtxt. It represents the maxixum universe that we have created for any skolemized lifetimes. When the infcx is first created, it will begin at UniverseIndex::ROOT. In later steps, qach time we create a skolemized lifetime, we will (a) increment the field and (b) use the new value (post-increment) as the universe of that lifetime.

pick de2dcd6d48 add universes to type inference variables

This gives each type inference variable a notion of universe but doesn't do anything with it. Unlike in the commit, though, we don't fetch the "current universe" from the parameter environment, but rather from the infcx -- this will actually make it much easier, because (for example) I don't think we have a need to make next_ty_var take a universe parameter. Instead, it can just read the "current universe" field of the infcx.

(Note: This relies on that "never interacts with siblings" property that I told you about before. That is, if we are trying to prove something like for<A> { ... }, we will increment the (global-ish) universe counter (say, to 1). If we then try to prove a sibling like exists<B> { ... }, the counter is still incremented, and hence B is instantiated with universe index 1 (not 0). But that's ok because 1 can still name everything from 0, and there should be no way for B to come in contact with A.)

pick: 12a230562e change skolemizations to use universe index

Let's take this commit, though it's sort of confusing "side step". All it does is to change the representation of a skolemized region (in particular, the ReSkolemized variant) to use a UniverseIndex -- but the source of that universe index is not the inference context, which is what we eventually want, but rather an internal counter in the region inference context. We'll patch that up later. But picking it ought to help with later picks and avoid confusing diffs.

pick 785c3610f4 store RegionVariableInfo and not just RegionVariableOrigin pick c3f515bd3c give a universe to region variables

Rebase these two commits, except, as above, we will modify them to use the universe index from the inference context.

pick 57c8cba6a5 make solving "universe aware", in a simplistic way

This simple change says that if you have a constraint like

exists<'a> { for<'b> { 'a: 'b } }

you can solve it by making 'a static. This is "good enough" for now, though not super smart, since for example

exists<'a> { for<'b> { if ('a: 'b) { 'a: 'b } } }

will still force 'a to be 'static, though it should not. (We don't intend to fix that in this PR series; current rustc kind of sidesteps the need to consider such concerns at the moment.)

new commit: kill higher_ranked_lub and higher_ranked_glb

If you look in src/librustc/infer/lub.rs, you'll see a routine called binders. Inside there is some older code that invokes higher_ranked_lub. That code is currently only used to generate the was_error variable, which is in turn used to give a better hint. You can kill that hint now, it's been long enough, and in the process remove the higher_ranked_lub fn. Then do the same analogous thing but for the binders method in glb.rs, which should let you kill the higher_ranked_glb fn. Once we've done that, don't forget to remove the OldStyleLUB variant. This may create some other amount of dead code.

Incidentally, this also fixes rust-lang/rust#45852.

pick 582ff87313 remove hr_match -- no longer needed

This cleans up an unrelated area of the code, but one that would be annoying.

pick b2f4105cf1 move param-env from CombineFields into the individual operations

We're not going to need this in this patch series, but we should do it anyway, because we'll need it later. It removes the assumption that the parameter environment stays the same all throughout subtyping.

pick 5f72a06d46 track skol levels in the ParamEnv rather than via counter

This one you can't really cherry-pick, because we are doing it differently, but conceptually it does what we want. The key change here is this one:

modified   src/librustc/infer/higher_ranked/mod.rs
@@ -589,13 +589,15 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
     ///
     /// See `README.md` for more details.
     pub fn skolemize_late_bound_regions<T>(&self,
-                                           binder: &ty::Binder<T>,
-                                           snapshot: &CombinedSnapshot<'a, 'tcx>)
-                                           -> (T, SkolemizationMap<'tcx>)
+                                           mut param_env: ty::ParamEnv<'tcx>,
+                                           binder: &ty::Binder<T>)
+                                           -> (T, ty::ParamEnv<'tcx>, SkolemizationMap<'tcx>)
         where T : TypeFoldable<'tcx>
     {
         let (result, map) = self.tcx.replace_late_bound_regions(binder, |br| {
-            self.region_vars.push_skolemized(br, &snapshot.region_vars_snapshot)
+            let (p, value) = self.tcx.mk_skolemized_region(param_env, br);
+            param_env = p;
+            value
         });
 
         debug!("skolemize_bound_regions(binder={:?}, result={:?}, map={:?})",

This method converts a type like for<'a> fn(&'a u32) into fn(&!a u32) (that is, it removes the binders, and replaces the regions bound in those binders with ReSkolemized regions). We want to keep that same operation, except we don't need to get the parameter environment from param_env and hence we don't need to thread the param_env through. Instead, for each skolemized region, we just make a fresh universe from the inference context.

pick b02f6c9fa2 remove pop_skolemized and friends pick 5936311b25 kill pop_skolemized() in region_inference pick cfbc5364ed region_inference: make some things private

That's all dead code now.

pick 7efe03f9f7 we now handle higher-ranked subtyping correctly

Update some test cases that are affected.

pick 21222fda4d FIXME: hack up the error messages so that compile-fail passes

We'll probably need this.

OK, at this point, I think we're done.