From ad91883624b0e5a7559acab56f912ccbe3a74376 Mon Sep 17 00:00:00 2001 From: "leonardo.yvens" Date: Tue, 5 Jun 2018 14:53:00 -0300 Subject: [PATCH 1/6] add `UniversalIndex` and use it in `Lifetime::ForAll` Compiles and tests but isn't ready for multiple lifetimes yet --- chalk-ir/src/debug.rs | 2 +- chalk-ir/src/fold.rs | 2 +- chalk-ir/src/lib.rs | 15 ++++++++++-- chalk-ir/src/macros.rs | 2 +- chalk-solve/src/infer/instantiate.rs | 2 +- chalk-solve/src/infer/test.rs | 2 +- chalk-solve/src/infer/unify.rs | 16 ++++++------- .../src/solve/slg/implementation/aggregate.rs | 4 ++-- .../src/solve/slg/implementation/resolvent.rs | 4 ++-- chalk-solve/src/solve/slg/test.rs | 2 +- chalk-solve/src/solve/test.rs | 24 +++++++++---------- 11 files changed, 43 insertions(+), 32 deletions(-) diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index 37188bc232b..bec6a4abf3a 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -60,7 +60,7 @@ impl Debug for Lifetime { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { match self { Lifetime::Var(depth) => write!(fmt, "'?{}", depth), - Lifetime::ForAll(universe) => write!(fmt, "'!{}", universe.counter), + Lifetime::ForAll(UniversalIndex { ui, idx }) => write!(fmt, "'!{}'{}", ui.counter, idx), } } } diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs index cd13e7de111..b9804892d96 100644 --- a/chalk-ir/src/fold.rs +++ b/chalk-ir/src/fold.rs @@ -349,7 +349,7 @@ pub fn super_fold_lifetime( } else { Ok(Lifetime::Var(depth)) }, - Lifetime::ForAll(universe) => folder.fold_free_universal_lifetime(universe, binders), + Lifetime::ForAll(universe) => folder.fold_free_universal_lifetime(universe.ui, binders), } } diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index d0dda852152..0a05fec0ca2 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -135,7 +135,7 @@ impl UniverseIndex { } pub fn to_lifetime(self) -> Lifetime { - Lifetime::ForAll(self) + Lifetime::ForAll(UniversalIndex { ui: self, idx: 0 }) } pub fn next(self) -> UniverseIndex { @@ -206,7 +206,18 @@ pub struct QuantifiedTy { pub enum Lifetime { /// See Ty::Var(_). Var(usize), - ForAll(UniverseIndex), + ForAll(UniversalIndex), +} + +/// Index of an universally quantified parameter in the environment. +/// Two indexes are required, the one of the universe itself +/// and the relative index inside the universe. +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct UniversalIndex { + /// Index *of* the universe. + pub ui: UniverseIndex, + /// Index *in* the universe. + pub idx: usize, } #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] diff --git a/chalk-ir/src/macros.rs b/chalk-ir/src/macros.rs index f6125a6f2c7..9c0c02d14c9 100644 --- a/chalk-ir/src/macros.rs +++ b/chalk-ir/src/macros.rs @@ -54,7 +54,7 @@ macro_rules! lifetime { }; (skol $b:expr) => { - $crate::Lifetime::ForAll(UniverseIndex { counter: $b }) + $crate::Lifetime::ForAll(UniversalIndex { ui: UniverseIndex { counter: $b }, idx: 0}) }; (expr $b:expr) => { diff --git a/chalk-solve/src/infer/instantiate.rs b/chalk-solve/src/infer/instantiate.rs index f912a78b40f..43af70b3a32 100644 --- a/chalk-solve/src/infer/instantiate.rs +++ b/chalk-solve/src/infer/instantiate.rs @@ -106,7 +106,7 @@ impl InferenceTable { let new_universe = self.new_universe(); match *pk { ParameterKind::Lifetime(()) => { - let lt = Lifetime::ForAll(new_universe); + let lt = Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }); ParameterKind::Lifetime(lt) } ParameterKind::Ty(()) => ParameterKind::Ty(Ty::Apply(ApplicationTy { diff --git a/chalk-solve/src/infer/test.rs b/chalk-solve/src/infer/test.rs index df69137be1f..e6cd55e9fac 100644 --- a/chalk-solve/src/infer/test.rs +++ b/chalk-solve/src/infer/test.rs @@ -294,6 +294,6 @@ fn lifetime_constraint_indirect() { assert_eq!(constraints.len(), 1); assert_eq!( format!("{:?}", constraints[0]), - "InEnvironment { environment: Env([]), goal: \'?2 == \'!1 }", + "InEnvironment { environment: Env([]), goal: \'?2 == \'!1'0 }", ); } diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index a1ef9dcb585..23589c872dc 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -178,7 +178,7 @@ impl<'t> Unifier<'t> { let lifetimes1: Vec<_> = (0..ty1.num_binders) .map(|_| { let new_universe = self.table.new_universe(); - Lifetime::ForAll(new_universe).cast() + Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }).cast() }) .collect(); @@ -242,7 +242,7 @@ impl<'t> Unifier<'t> { let lifetimes1: Vec<_> = (0..ty1.num_binders) .map(|_| { let new_universe = self.table.new_universe(); - Lifetime::ForAll(new_universe).cast() + Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }).cast() }) .collect(); @@ -294,16 +294,16 @@ impl<'t> Unifier<'t> { Ok(()) } - (&Lifetime::Var(depth), &Lifetime::ForAll(ui)) - | (&Lifetime::ForAll(ui), &Lifetime::Var(depth)) => { + (&Lifetime::Var(depth), &Lifetime::ForAll(idx)) + | (&Lifetime::ForAll(idx), &Lifetime::Var(depth)) => { let var = InferenceVariable::from_depth(depth); let var_ui = self.table.universe_of_unbound_var(var); - if var_ui.can_see(ui) { + if var_ui.can_see(idx.ui) { debug!( "unify_lifetime_lifetime: {:?} in {:?} can see {:?}; unifying", - var, var_ui, ui + var, var_ui, idx.ui ); - let v = Lifetime::ForAll(ui); + let v = Lifetime::ForAll(idx); self.table .unify .unify_var_value(var, InferenceValue::from(v)) @@ -312,7 +312,7 @@ impl<'t> Unifier<'t> { } else { debug!( "unify_lifetime_lifetime: {:?} in {:?} cannot see {:?}; pushing constraint", - var, var_ui, ui + var, var_ui, idx.ui ); Ok(self.push_lifetime_eq_constraint(*a, *b)) } diff --git a/chalk-solve/src/solve/slg/implementation/aggregate.rs b/chalk-solve/src/solve/slg/implementation/aggregate.rs index c3679ecac8e..77c10f6641c 100644 --- a/chalk-solve/src/solve/slg/implementation/aggregate.rs +++ b/chalk-solve/src/solve/slg/implementation/aggregate.rs @@ -320,8 +320,8 @@ impl<'infer> AntiUnifier<'infer> { match (l1, l2) { (Lifetime::Var(_), _) | (_, Lifetime::Var(_)) => self.new_lifetime_variable(), - (Lifetime::ForAll(ui1), Lifetime::ForAll(ui2)) => if ui1 == ui2 { - Lifetime::ForAll(*ui1) + (Lifetime::ForAll(_), Lifetime::ForAll(_)) => if l1 == l2 { + *l1 } else { self.new_lifetime_variable() }, diff --git a/chalk-solve/src/solve/slg/implementation/resolvent.rs b/chalk-solve/src/solve/slg/implementation/resolvent.rs index e1146103568..3a7a3789033 100644 --- a/chalk-solve/src/solve/slg/implementation/resolvent.rs +++ b/chalk-solve/src/solve/slg/implementation/resolvent.rs @@ -388,8 +388,8 @@ impl<'t> Zipper for AnswerSubstitutor<'t> { self.assert_matching_vars(*answer_depth, *pending_depth) } - (Lifetime::ForAll(answer_ui), Lifetime::ForAll(pending_ui)) => { - assert_eq!(answer_ui, pending_ui); + (Lifetime::ForAll(_), Lifetime::ForAll(_)) => { + assert_eq!(answer, pending); Ok(()) } diff --git a/chalk-solve/src/solve/slg/test.rs b/chalk-solve/src/solve/slg/test.rs index 203a562d3a5..90f23c3ea3f 100644 --- a/chalk-solve/src/solve/slg/test.rs +++ b/chalk-solve/src/solve/slg/test.rs @@ -550,7 +550,7 @@ fn basic_region_constraint_from_positive_impl() { constraints: [ InEnvironment { environment: Env([]), - goal: '!2 == '!1 + goal: '!2'0 == '!1'0 } ] }, diff --git a/chalk-solve/src/solve/test.rs b/chalk-solve/src/solve/test.rs index 116aab095bd..3b9c685bea4 100644 --- a/chalk-solve/src/solve/test.rs +++ b/chalk-solve/src/solve/test.rs @@ -581,7 +581,7 @@ fn normalize_gat1() { } } } yields { - "Unique; substitution [?0 := Iter<'!2, !1>], lifetime constraints []" + "Unique; substitution [?0 := Iter<'!2'0, !1>], lifetime constraints []" } } } @@ -606,7 +606,7 @@ fn normalize_gat2() { } } } yields { - "Unique; substitution [?0 := Span<'!1, !2>], lifetime constraints []" + "Unique; substitution [?0 := Span<'!1'0, !2>], lifetime constraints []" } goal { @@ -922,7 +922,7 @@ fn region_equality() { } yields { "Unique; substitution [], lifetime constraints \ - [InEnvironment { environment: Env([]), goal: '!2 == '!1 }] + [InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }] " } @@ -933,7 +933,7 @@ fn region_equality() { } } } yields { - "Unique; substitution [?0 := '!1], lifetime constraints []" + "Unique; substitution [?0 := '!1'0], lifetime constraints []" } } } @@ -971,7 +971,7 @@ fn forall_equality() { for<'c, 'd> Ref<'c, Ref<'d, Ref<'d, Unit>>>> } yields { "Unique; substitution [], lifetime constraints [ - InEnvironment { environment: Env([]), goal: '!2 == '!1 } + InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 } ]" } } @@ -1185,7 +1185,7 @@ fn normalize_under_binder() { } } } yields { - "Unique; substitution [?0 := Ref<'!1, I32>], lifetime constraints []" + "Unique; substitution [?0 := Ref<'!1'0, I32>], lifetime constraints []" } goal { @@ -1197,7 +1197,7 @@ fn normalize_under_binder() { } yields { "Unique; for { \ substitution [?0 := Ref<'?0, I32>], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \ }" } } @@ -1221,7 +1221,7 @@ fn unify_quantified_lifetimes() { } yields { "Unique; for { \ substitution [?0 := '?0], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \ }" } @@ -1237,8 +1237,8 @@ fn unify_quantified_lifetimes() { } } yields { "Unique; for { \ - substitution [?0 := '?0, ?1 := '!1], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \ + substitution [?0 := '?0, ?1 := '!1'0], \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \ }" } } @@ -1263,7 +1263,7 @@ fn equality_binder() { } yields { "Unique; for { \ substitution [?0 := '?0], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '!2 == '?0 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '!2'0 == '?0 }] \ }" } } @@ -2394,7 +2394,7 @@ fn quantified_types() { } yields { // Lifetime constraints are unsatisfiable "Unique; substitution [], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '!2 == '!1 }]" + lifetime constraints [InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }]" } } } From 82bf5d6cf9e7117fccfe5f004eb27788b7c75951 Mon Sep 17 00:00:00 2001 From: "leonardo.yvens" Date: Tue, 5 Jun 2018 15:32:15 -0300 Subject: [PATCH 2/6] Refactor `fold_free_universal_lifetime` to take a `UniversalIndex` --- chalk-ir/src/fold.rs | 6 +++--- chalk-ir/src/lib.rs | 10 ++++++---- chalk-solve/src/infer/canonicalize.rs | 4 ++-- chalk-solve/src/infer/invert.rs | 6 +++--- chalk-solve/src/infer/ucanonicalize.rs | 16 ++++++++-------- chalk-solve/src/infer/unify.rs | 4 ++-- 6 files changed, 24 insertions(+), 22 deletions(-) diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs index b9804892d96..d21cd50d2b1 100644 --- a/chalk-ir/src/fold.rs +++ b/chalk-ir/src/fold.rs @@ -140,7 +140,7 @@ pub trait UniversalFolder { /// As with `fold_free_universal_ty`, but for lifetimes. fn fold_free_universal_lifetime( &mut self, - universe: UniverseIndex, + universe: UniversalIndex, binders: usize, ) -> Fallible; } @@ -157,7 +157,7 @@ impl UniversalFolder for T { fn fold_free_universal_lifetime( &mut self, - universe: UniverseIndex, + universe: UniversalIndex, _binders: usize, ) -> Fallible { Ok(universe.to_lifetime()) @@ -349,7 +349,7 @@ pub fn super_fold_lifetime( } else { Ok(Lifetime::Var(depth)) }, - Lifetime::ForAll(universe) => folder.fold_free_universal_lifetime(universe.ui, binders), + Lifetime::ForAll(universe) => folder.fold_free_universal_lifetime(universe, binders), } } diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 0a05fec0ca2..8ae6c41430e 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -134,10 +134,6 @@ impl UniverseIndex { self.counter >= ui.counter } - pub fn to_lifetime(self) -> Lifetime { - Lifetime::ForAll(UniversalIndex { ui: self, idx: 0 }) - } - pub fn next(self) -> UniverseIndex { UniverseIndex { counter: self.counter + 1, @@ -220,6 +216,12 @@ pub struct UniversalIndex { pub idx: usize, } +impl UniversalIndex { + pub fn to_lifetime(self) -> Lifetime { + Lifetime::ForAll(self) + } +} + #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] pub struct ApplicationTy { pub name: TypeName, diff --git a/chalk-solve/src/infer/canonicalize.rs b/chalk-solve/src/infer/canonicalize.rs index d296ffa946d..d07f2df2f95 100644 --- a/chalk-solve/src/infer/canonicalize.rs +++ b/chalk-solve/src/infer/canonicalize.rs @@ -101,10 +101,10 @@ impl<'q> UniversalFolder for Canonicalizer<'q> { fn fold_free_universal_lifetime( &mut self, - universe: UniverseIndex, + universe: UniversalIndex, _binders: usize, ) -> Fallible { - self.max_universe = max(self.max_universe, universe); + self.max_universe = max(self.max_universe, universe.ui); Ok(universe.to_lifetime()) } } diff --git a/chalk-solve/src/infer/invert.rs b/chalk-solve/src/infer/invert.rs index a1651bc0c11..dedc47fc198 100644 --- a/chalk-solve/src/infer/invert.rs +++ b/chalk-solve/src/infer/invert.rs @@ -98,7 +98,7 @@ impl InferenceTable { struct Inverter<'q> { table: &'q mut InferenceTable, inverted_ty: HashMap, - inverted_lifetime: HashMap, + inverted_lifetime: HashMap, } impl<'q> Inverter<'q> { @@ -127,14 +127,14 @@ impl<'q> UniversalFolder for Inverter<'q> { fn fold_free_universal_lifetime( &mut self, - universe: UniverseIndex, + universe: UniversalIndex, binders: usize, ) -> Fallible { let table = &mut self.table; Ok( self.inverted_lifetime .entry(universe) - .or_insert_with(|| table.new_variable(universe)) + .or_insert_with(|| table.new_variable(universe.ui)) .to_lifetime() .shifted_in(binders), ) diff --git a/chalk-solve/src/infer/ucanonicalize.rs b/chalk-solve/src/infer/ucanonicalize.rs index 3c7c09f35cf..065b3c83387 100644 --- a/chalk-solve/src/infer/ucanonicalize.rs +++ b/chalk-solve/src/infer/ucanonicalize.rs @@ -227,10 +227,10 @@ impl<'q> UniversalFolder for UCollector<'q> { fn fold_free_universal_lifetime( &mut self, - universe: UniverseIndex, + universe: UniversalIndex, _binders: usize, ) -> Fallible { - self.universes.add(universe); + self.universes.add(universe.ui); Ok(universe.to_lifetime()) } } @@ -255,11 +255,11 @@ impl<'q> UniversalFolder for UMapToCanonical<'q> { fn fold_free_universal_lifetime( &mut self, - universe0: UniverseIndex, + universe0: UniversalIndex, _binders: usize, ) -> Fallible { - let universe = self.universes.map_universe_to_canonical(universe0); - Ok(universe.to_lifetime()) + let universe = self.universes.map_universe_to_canonical(universe0.ui); + Ok(UniversalIndex { ui: universe, idx: universe0.idx }.to_lifetime()) } } @@ -283,11 +283,11 @@ impl<'q> UniversalFolder for UMapFromCanonical<'q> { fn fold_free_universal_lifetime( &mut self, - universe0: UniverseIndex, + universe0: UniversalIndex, _binders: usize, ) -> Fallible { - let universe = self.universes.map_universe_from_canonical(universe0); - Ok(universe.to_lifetime()) + let universe = self.universes.map_universe_from_canonical(universe0.ui); + Ok(UniversalIndex { ui: universe, idx: universe0.idx }.to_lifetime()) } } diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index 23589c872dc..0af080306ec 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -384,10 +384,10 @@ impl<'u, 't> UniversalFolder for OccursCheck<'u, 't> { fn fold_free_universal_lifetime( &mut self, - ui: UniverseIndex, + ui: UniversalIndex, binders: usize, ) -> Fallible { - if self.universe_index < ui { + if self.universe_index < ui.ui { // Scenario is like: // // exists forall<'b> ?T = Foo<'b> From c8b2882ea362080a1bb544edcf739770b5ffaf4d Mon Sep 17 00:00:00 2001 From: "leonardo.yvens" Date: Tue, 5 Jun 2018 16:19:38 -0300 Subject: [PATCH 3/6] Pack lifetimes from the same binder into the same universe This changes the output of some tests, should not alter any semantics --- chalk-solve/src/infer/instantiate.rs | 17 +++++++++++------ chalk-solve/src/infer/unify.rs | 11 +++++++---- chalk-solve/src/solve/slg/test.rs | 2 +- chalk-solve/src/solve/test.rs | 6 +++--- 4 files changed, 22 insertions(+), 14 deletions(-) diff --git a/chalk-solve/src/infer/instantiate.rs b/chalk-solve/src/infer/instantiate.rs index 43af70b3a32..9afc1c0d3da 100644 --- a/chalk-solve/src/infer/instantiate.rs +++ b/chalk-solve/src/infer/instantiate.rs @@ -100,19 +100,24 @@ impl InferenceTable { T: Fold, { let (binders, value) = arg.split(); + let lifetime_ui = self.new_universe(); + let mut idx = 0; let parameters: Vec<_> = binders .iter() .map(|pk| { - let new_universe = self.new_universe(); match *pk { ParameterKind::Lifetime(()) => { - let lt = Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }); + let lt = Lifetime::ForAll(UniversalIndex { ui: lifetime_ui, idx }); + idx += 1; ParameterKind::Lifetime(lt) } - ParameterKind::Ty(()) => ParameterKind::Ty(Ty::Apply(ApplicationTy { - name: TypeName::ForAll(new_universe), - parameters: vec![], - })), + ParameterKind::Ty(()) => { + let new_universe = self.new_universe(); + ParameterKind::Ty(Ty::Apply(ApplicationTy { + name: TypeName::ForAll(new_universe), + parameters: vec![], + })) + } } }) .collect(); diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index 0af080306ec..8c948397243 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -166,19 +166,22 @@ impl<'t> Unifier<'t> { } fn unify_forall_tys(&mut self, ty1: &QuantifiedTy, ty2: &QuantifiedTy) -> Fallible<()> { - // for<'a...> T == for<'b...> U where 'a != 'b + // for<'a...> T == for<'b...> U // // if: // // for<'a...> exists<'b...> T == U && // for<'b...> exists<'a...> T == U + // + // Here we only check for<'a...> exists<'b...> T == U, + // can someone smart comment why this is sufficient? debug!("unify_forall_tys({:?}, {:?})", ty1, ty2); + let ui = self.table.new_universe(); let lifetimes1: Vec<_> = (0..ty1.num_binders) - .map(|_| { - let new_universe = self.table.new_universe(); - Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }).cast() + .map(|idx| { + Lifetime::ForAll(UniversalIndex { ui, idx }).cast() }) .collect(); diff --git a/chalk-solve/src/solve/slg/test.rs b/chalk-solve/src/solve/slg/test.rs index 90f23c3ea3f..d808c379289 100644 --- a/chalk-solve/src/solve/slg/test.rs +++ b/chalk-solve/src/solve/slg/test.rs @@ -550,7 +550,7 @@ fn basic_region_constraint_from_positive_impl() { constraints: [ InEnvironment { environment: Env([]), - goal: '!2'0 == '!1'0 + goal: '!1'1 == '!1'0 } ] }, diff --git a/chalk-solve/src/solve/test.rs b/chalk-solve/src/solve/test.rs index 3b9c685bea4..793a6b908f5 100644 --- a/chalk-solve/src/solve/test.rs +++ b/chalk-solve/src/solve/test.rs @@ -922,7 +922,7 @@ fn region_equality() { } yields { "Unique; substitution [], lifetime constraints \ - [InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }] + [InEnvironment { environment: Env([]), goal: '!1'1 == '!1'0 }] " } @@ -966,12 +966,12 @@ fn forall_equality() { // this is because the region constraints are unsolvable. // // Note that `?0` (in universe 2) must be equal to both - // `!1` and `!2`, which of course it cannot be. + // `!1'0` and `!1'1`, which of course it cannot be. for<'a, 'b> Ref<'a, Ref<'b, Ref<'a, Unit>>>: Eq< for<'c, 'd> Ref<'c, Ref<'d, Ref<'d, Unit>>>> } yields { "Unique; substitution [], lifetime constraints [ - InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 } + InEnvironment { environment: Env([]), goal: '!1'1 == '!1'0 } ]" } } From ea09744f25d4a0cd129dbce5dde53473e03b2762 Mon Sep 17 00:00:00 2001 From: "leonardo.yvens" Date: Wed, 6 Jun 2018 08:02:15 -0300 Subject: [PATCH 4/6] Universal indexing: change 1'0 to 1_0, leverage it in `unify_forall_apply` --- chalk-ir/src/debug.rs | 2 +- chalk-solve/src/infer/test.rs | 2 +- chalk-solve/src/infer/unify.rs | 6 +++--- chalk-solve/src/solve/slg/test.rs | 2 +- chalk-solve/src/solve/test.rs | 26 +++++++++++++------------- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index bec6a4abf3a..20f64949f6f 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -60,7 +60,7 @@ impl Debug for Lifetime { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { match self { Lifetime::Var(depth) => write!(fmt, "'?{}", depth), - Lifetime::ForAll(UniversalIndex { ui, idx }) => write!(fmt, "'!{}'{}", ui.counter, idx), + Lifetime::ForAll(UniversalIndex { ui, idx }) => write!(fmt, "'!{}_{}", ui.counter, idx), } } } diff --git a/chalk-solve/src/infer/test.rs b/chalk-solve/src/infer/test.rs index e6cd55e9fac..3b1cb136d70 100644 --- a/chalk-solve/src/infer/test.rs +++ b/chalk-solve/src/infer/test.rs @@ -294,6 +294,6 @@ fn lifetime_constraint_indirect() { assert_eq!(constraints.len(), 1); assert_eq!( format!("{:?}", constraints[0]), - "InEnvironment { environment: Env([]), goal: \'?2 == \'!1'0 }", + "InEnvironment { environment: Env([]), goal: \'?2 == \'!1_0 }", ); } diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index 8c948397243..eaad47d0b5c 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -242,10 +242,10 @@ impl<'t> Unifier<'t> { } fn unify_forall_apply(&mut self, ty1: &QuantifiedTy, ty2: &Ty) -> Fallible<()> { + let ui = self.table.new_universe(); let lifetimes1: Vec<_> = (0..ty1.num_binders) - .map(|_| { - let new_universe = self.table.new_universe(); - Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }).cast() + .map(|idx| { + Lifetime::ForAll(UniversalIndex { ui, idx }).cast() }) .collect(); diff --git a/chalk-solve/src/solve/slg/test.rs b/chalk-solve/src/solve/slg/test.rs index d808c379289..9e203c36f9f 100644 --- a/chalk-solve/src/solve/slg/test.rs +++ b/chalk-solve/src/solve/slg/test.rs @@ -550,7 +550,7 @@ fn basic_region_constraint_from_positive_impl() { constraints: [ InEnvironment { environment: Env([]), - goal: '!1'1 == '!1'0 + goal: '!1_1 == '!1_0 } ] }, diff --git a/chalk-solve/src/solve/test.rs b/chalk-solve/src/solve/test.rs index 793a6b908f5..9c7dca9e799 100644 --- a/chalk-solve/src/solve/test.rs +++ b/chalk-solve/src/solve/test.rs @@ -581,7 +581,7 @@ fn normalize_gat1() { } } } yields { - "Unique; substitution [?0 := Iter<'!2'0, !1>], lifetime constraints []" + "Unique; substitution [?0 := Iter<'!2_0, !1>], lifetime constraints []" } } } @@ -606,7 +606,7 @@ fn normalize_gat2() { } } } yields { - "Unique; substitution [?0 := Span<'!1'0, !2>], lifetime constraints []" + "Unique; substitution [?0 := Span<'!1_0, !2>], lifetime constraints []" } goal { @@ -922,7 +922,7 @@ fn region_equality() { } yields { "Unique; substitution [], lifetime constraints \ - [InEnvironment { environment: Env([]), goal: '!1'1 == '!1'0 }] + [InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }] " } @@ -933,7 +933,7 @@ fn region_equality() { } } } yields { - "Unique; substitution [?0 := '!1'0], lifetime constraints []" + "Unique; substitution [?0 := '!1_0], lifetime constraints []" } } } @@ -966,12 +966,12 @@ fn forall_equality() { // this is because the region constraints are unsolvable. // // Note that `?0` (in universe 2) must be equal to both - // `!1'0` and `!1'1`, which of course it cannot be. + // `!1_0` and `!1_1`, which of course it cannot be. for<'a, 'b> Ref<'a, Ref<'b, Ref<'a, Unit>>>: Eq< for<'c, 'd> Ref<'c, Ref<'d, Ref<'d, Unit>>>> } yields { "Unique; substitution [], lifetime constraints [ - InEnvironment { environment: Env([]), goal: '!1'1 == '!1'0 } + InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 } ]" } } @@ -1185,7 +1185,7 @@ fn normalize_under_binder() { } } } yields { - "Unique; substitution [?0 := Ref<'!1'0, I32>], lifetime constraints []" + "Unique; substitution [?0 := Ref<'!1_0, I32>], lifetime constraints []" } goal { @@ -1197,7 +1197,7 @@ fn normalize_under_binder() { } yields { "Unique; for { \ substitution [?0 := Ref<'?0, I32>], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \ }" } } @@ -1221,7 +1221,7 @@ fn unify_quantified_lifetimes() { } yields { "Unique; for { \ substitution [?0 := '?0], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \ }" } @@ -1237,8 +1237,8 @@ fn unify_quantified_lifetimes() { } } yields { "Unique; for { \ - substitution [?0 := '?0, ?1 := '!1'0], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \ + substitution [?0 := '?0, ?1 := '!1_0], \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \ }" } } @@ -1263,7 +1263,7 @@ fn equality_binder() { } yields { "Unique; for { \ substitution [?0 := '?0], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '!2'0 == '?0 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '?0 }] \ }" } } @@ -2394,7 +2394,7 @@ fn quantified_types() { } yields { // Lifetime constraints are unsatisfiable "Unique; substitution [], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }]" + lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '!1_0 }]" } } } From 8157eeea515bf509ce6c4b24ac3631ee00a063e5 Mon Sep 17 00:00:00 2001 From: "leonardo.yvens" Date: Wed, 6 Jun 2018 08:55:42 -0300 Subject: [PATCH 5/6] One universe many types --- chalk-ir/src/debug.rs | 2 +- chalk-ir/src/fold.rs | 6 +++--- chalk-ir/src/lib.rs | 18 ++++++++---------- chalk-ir/src/macros.rs | 7 ++++++- chalk-solve/src/infer/canonicalize.rs | 6 +++--- chalk-solve/src/infer/instantiate.rs | 18 ++++++------------ chalk-solve/src/infer/invert.rs | 6 +++--- chalk-solve/src/infer/ucanonicalize.rs | 18 +++++++++--------- chalk-solve/src/infer/unify.rs | 6 +++--- chalk-solve/src/solve/slg/test.rs | 2 +- chalk-solve/src/solve/test.rs | 14 +++++++------- 11 files changed, 50 insertions(+), 53 deletions(-) diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index 20f64949f6f..72502695c08 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -30,7 +30,7 @@ impl Debug for TypeName { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { match self { TypeName::ItemId(id) => write!(fmt, "{:?}", id), - TypeName::ForAll(universe) => write!(fmt, "!{}", universe.counter), + TypeName::ForAll(universe) => write!(fmt, "!{}_{}", universe.ui.counter, universe.idx), TypeName::AssociatedType(assoc_ty) => write!(fmt, "{:?}", assoc_ty), } } diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs index d21cd50d2b1..f7b5a1bc7b8 100644 --- a/chalk-ir/src/fold.rs +++ b/chalk-ir/src/fold.rs @@ -135,7 +135,7 @@ pub trait UniversalFolder { /// /// - `universe` is the universe of the `TypeName::ForAll` that was found /// - `binders` is the number of binders in scope - fn fold_free_universal_ty(&mut self, universe: UniverseIndex, binders: usize) -> Fallible; + fn fold_free_universal_ty(&mut self, universe: UniversalIndex, binders: usize) -> Fallible; /// As with `fold_free_universal_ty`, but for lifetimes. fn fold_free_universal_lifetime( @@ -151,8 +151,8 @@ pub trait UniversalFolder { pub trait IdentityUniversalFolder {} impl UniversalFolder for T { - fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible { - Ok(TypeName::ForAll(universe).to_ty()) + fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible { + Ok(universe.to_ty()) } fn fold_free_universal_lifetime( diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index 8ae6c41430e..13520cf16ac 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -96,21 +96,12 @@ pub enum TypeName { ItemId(ItemId), /// skolemized form of a type parameter like `T` - ForAll(UniverseIndex), + ForAll(UniversalIndex), /// an associated type like `Iterator::Item`; see `AssociatedType` for details AssociatedType(ItemId), } -impl TypeName { - pub fn to_ty(self) -> Ty { - Ty::Apply(ApplicationTy { - name: self, - parameters: vec![], - }) - } -} - /// An universe index is how a universally quantified parameter is /// represented when it's binder is moved into the environment. /// An example chain of transformations would be: @@ -220,6 +211,13 @@ impl UniversalIndex { pub fn to_lifetime(self) -> Lifetime { Lifetime::ForAll(self) } + + pub fn to_ty(self) -> Ty { + Ty::Apply(ApplicationTy { + name: TypeName::ForAll(self), + parameters: vec![], + }) + } } #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] diff --git a/chalk-ir/src/macros.rs b/chalk-ir/src/macros.rs index 9c0c02d14c9..3ef1229d7cc 100644 --- a/chalk-ir/src/macros.rs +++ b/chalk-ir/src/macros.rs @@ -69,5 +69,10 @@ macro_rules! lifetime { #[macro_export] macro_rules! ty_name { ((item $n:expr)) => { $crate::TypeName::ItemId(ItemId { index: $n }) }; - ((skol $n:expr)) => { $crate::TypeName::ForAll(UniverseIndex { counter: $n }) } + ((skol $n:expr)) => { $crate::TypeName::ForAll( + UniversalIndex { + ui: UniverseIndex { counter: $n }, + idx: 0, + }) + } } diff --git a/chalk-solve/src/infer/canonicalize.rs b/chalk-solve/src/infer/canonicalize.rs index d07f2df2f95..731602e2982 100644 --- a/chalk-solve/src/infer/canonicalize.rs +++ b/chalk-solve/src/infer/canonicalize.rs @@ -94,9 +94,9 @@ impl<'q> Canonicalizer<'q> { impl<'q> DefaultTypeFolder for Canonicalizer<'q> {} impl<'q> UniversalFolder for Canonicalizer<'q> { - fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible { - self.max_universe = max(self.max_universe, universe); - Ok(TypeName::ForAll(universe).to_ty()) + fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible { + self.max_universe = max(self.max_universe, universe.ui); + Ok(universe.to_ty()) } fn fold_free_universal_lifetime( diff --git a/chalk-solve/src/infer/instantiate.rs b/chalk-solve/src/infer/instantiate.rs index 9afc1c0d3da..5a9d6347a63 100644 --- a/chalk-solve/src/infer/instantiate.rs +++ b/chalk-solve/src/infer/instantiate.rs @@ -100,24 +100,18 @@ impl InferenceTable { T: Fold, { let (binders, value) = arg.split(); - let lifetime_ui = self.new_universe(); - let mut idx = 0; + let ui = self.new_universe(); let parameters: Vec<_> = binders .iter() - .map(|pk| { + .enumerate() + .map(|(idx, pk)| { + let universal_idx = UniversalIndex { ui, idx }; match *pk { ParameterKind::Lifetime(()) => { - let lt = Lifetime::ForAll(UniversalIndex { ui: lifetime_ui, idx }); - idx += 1; + let lt = universal_idx.to_lifetime(); ParameterKind::Lifetime(lt) } - ParameterKind::Ty(()) => { - let new_universe = self.new_universe(); - ParameterKind::Ty(Ty::Apply(ApplicationTy { - name: TypeName::ForAll(new_universe), - parameters: vec![], - })) - } + ParameterKind::Ty(()) => ParameterKind::Ty(universal_idx.to_ty()), } }) .collect(); diff --git a/chalk-solve/src/infer/invert.rs b/chalk-solve/src/infer/invert.rs index dedc47fc198..1e2be4076e7 100644 --- a/chalk-solve/src/infer/invert.rs +++ b/chalk-solve/src/infer/invert.rs @@ -97,7 +97,7 @@ impl InferenceTable { struct Inverter<'q> { table: &'q mut InferenceTable, - inverted_ty: HashMap, + inverted_ty: HashMap, inverted_lifetime: HashMap, } @@ -114,12 +114,12 @@ impl<'q> Inverter<'q> { impl<'q> DefaultTypeFolder for Inverter<'q> {} impl<'q> UniversalFolder for Inverter<'q> { - fn fold_free_universal_ty(&mut self, universe: UniverseIndex, binders: usize) -> Fallible { + fn fold_free_universal_ty(&mut self, universe: UniversalIndex, binders: usize) -> Fallible { let table = &mut self.table; Ok( self.inverted_ty .entry(universe) - .or_insert_with(|| table.new_variable(universe)) + .or_insert_with(|| table.new_variable(universe.ui)) .to_ty() .shifted_in(binders), ) diff --git a/chalk-solve/src/infer/ucanonicalize.rs b/chalk-solve/src/infer/ucanonicalize.rs index 065b3c83387..5bc505c4460 100644 --- a/chalk-solve/src/infer/ucanonicalize.rs +++ b/chalk-solve/src/infer/ucanonicalize.rs @@ -220,9 +220,9 @@ struct UCollector<'q> { impl<'q> DefaultTypeFolder for UCollector<'q> {} impl<'q> UniversalFolder for UCollector<'q> { - fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible { - self.universes.add(universe); - Ok(TypeName::ForAll(universe).to_ty()) + fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible { + self.universes.add(universe.ui); + Ok(universe.to_ty()) } fn fold_free_universal_lifetime( @@ -246,11 +246,11 @@ impl<'q> DefaultTypeFolder for UMapToCanonical<'q> {} impl<'q> UniversalFolder for UMapToCanonical<'q> { fn fold_free_universal_ty( &mut self, - universe0: UniverseIndex, + universe0: UniversalIndex, _binders: usize, ) -> Fallible { - let universe = self.universes.map_universe_to_canonical(universe0); - Ok(TypeName::ForAll(universe).to_ty()) + let ui = self.universes.map_universe_to_canonical(universe0.ui); + Ok(UniversalIndex { ui, idx: universe0.idx }.to_ty()) } fn fold_free_universal_lifetime( @@ -274,11 +274,11 @@ impl<'q> DefaultTypeFolder for UMapFromCanonical<'q> {} impl<'q> UniversalFolder for UMapFromCanonical<'q> { fn fold_free_universal_ty( &mut self, - universe0: UniverseIndex, + universe0: UniversalIndex, _binders: usize, ) -> Fallible { - let universe = self.universes.map_universe_from_canonical(universe0); - Ok(TypeName::ForAll(universe).to_ty()) + let ui = self.universes.map_universe_from_canonical(universe0.ui); + Ok(UniversalIndex { ui, idx: universe0.idx }.to_ty()) } fn fold_free_universal_lifetime( diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index eaad47d0b5c..cbfac193b34 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -377,11 +377,11 @@ impl<'u, 't> OccursCheck<'u, 't> { impl<'u, 't> DefaultTypeFolder for OccursCheck<'u, 't> {} impl<'u, 't> UniversalFolder for OccursCheck<'u, 't> { - fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible { - if self.universe_index < universe { + fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible { + if self.universe_index < universe.ui { Err(NoSolution) } else { - Ok(TypeName::ForAll(universe).to_ty()) // no need to shift, not relative to depth + Ok(universe.to_ty()) // no need to shift, not relative to depth } } diff --git a/chalk-solve/src/solve/slg/test.rs b/chalk-solve/src/solve/slg/test.rs index 9e203c36f9f..d7018a44588 100644 --- a/chalk-solve/src/solve/slg/test.rs +++ b/chalk-solve/src/solve/slg/test.rs @@ -482,7 +482,7 @@ fn subgoal_cycle_uninhabited() { Answer { subst: Canonical { value: ConstrainedSubst { - subst: [?0 := !1], + subst: [?0 := !1_0], constraints: [] }, binders: [] diff --git a/chalk-solve/src/solve/test.rs b/chalk-solve/src/solve/test.rs index 9c7dca9e799..38800b2a5ff 100644 --- a/chalk-solve/src/solve/test.rs +++ b/chalk-solve/src/solve/test.rs @@ -476,7 +476,7 @@ fn normalize_basic() { } } } yields { - "Unique; substitution [?0 := !1], lifetime constraints []" + "Unique; substitution [?0 := !1_0], lifetime constraints []" } goal { @@ -506,7 +506,7 @@ fn normalize_basic() { } } } yields { - "Unique; substitution [?0 := (Iterator::Item)]" + "Unique; substitution [?0 := (Iterator::Item)]" } goal { @@ -518,7 +518,7 @@ fn normalize_basic() { } } } yields { - "Unique; substitution [?0 := (Iterator::Item)]" + "Unique; substitution [?0 := (Iterator::Item)]" } goal { @@ -581,7 +581,7 @@ fn normalize_gat1() { } } } yields { - "Unique; substitution [?0 := Iter<'!2_0, !1>], lifetime constraints []" + "Unique; substitution [?0 := Iter<'!2_0, !1_0>], lifetime constraints []" } } } @@ -606,7 +606,7 @@ fn normalize_gat2() { } } } yields { - "Unique; substitution [?0 := Span<'!1_0, !2>], lifetime constraints []" + "Unique; substitution [?0 := Span<'!1_0, !1_1>], lifetime constraints []" } goal { @@ -664,7 +664,7 @@ fn normalize_gat_with_where_clause() { } } } yields { - "Unique; substitution [?0 := Value]" + "Unique; substitution [?0 := Value]" } } } @@ -703,7 +703,7 @@ fn normalize_gat_with_where_clause2() { } } } yields { - "Unique; substitution [?0 := !2]" + "Unique; substitution [?0 := !1_1]" } } } From 8440ed8b161cd6f15ac9681e0cb06ae75b4f10e6 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Fri, 14 Sep 2018 15:45:51 -0400 Subject: [PATCH 6/6] update tests --- src/test.rs | 50 ++++++++++++++++++++++++------------------------- src/test/slg.rs | 4 ++-- 2 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/test.rs b/src/test.rs index f5c9dd12b3a..3d1eb450273 100644 --- a/src/test.rs +++ b/src/test.rs @@ -478,7 +478,7 @@ fn normalize_basic() { } } } yields { - "Unique; substitution [?0 := !1], lifetime constraints []" + "Unique; substitution [?0 := !1_0], lifetime constraints []" } goal { @@ -508,7 +508,7 @@ fn normalize_basic() { } } } yields { - "Unique; substitution [?0 := (Iterator::Item)]" + "Unique; substitution [?0 := (Iterator::Item)]" } goal { @@ -520,7 +520,7 @@ fn normalize_basic() { } } } yields { - "Unique; substitution [?0 := (Iterator::Item)]" + "Unique; substitution [?0 := (Iterator::Item)]" } goal { @@ -583,7 +583,7 @@ fn normalize_gat1() { } } } yields { - "Unique; substitution [?0 := Iter<'!2, !1>], lifetime constraints []" + "Unique; substitution [?0 := Iter<'!2_0, !1_0>], lifetime constraints []" } } } @@ -608,7 +608,7 @@ fn normalize_gat2() { } } } yields { - "Unique; substitution [?0 := Span<'!1, !2>], lifetime constraints []" + "Unique; substitution [?0 := Span<'!1_0, !1_1>], lifetime constraints []" } goal { @@ -666,7 +666,7 @@ fn normalize_gat_with_where_clause() { } } } yields { - "Unique; substitution [?0 := Value]" + "Unique; substitution [?0 := Value]" } } } @@ -705,7 +705,7 @@ fn normalize_gat_with_where_clause2() { } } } yields { - "Unique; substitution [?0 := !2]" + "Unique; substitution [?0 := !1_1]" } } } @@ -924,7 +924,7 @@ fn region_equality() { } yields { "Unique; substitution [], lifetime constraints \ - [InEnvironment { environment: Env([]), goal: '!2 == '!1 }] + [InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }] " } @@ -935,7 +935,7 @@ fn region_equality() { } } } yields { - "Unique; substitution [?0 := '!1], lifetime constraints []" + "Unique; substitution [?0 := '!1_0], lifetime constraints []" } } } @@ -968,12 +968,12 @@ fn forall_equality() { // this is because the region constraints are unsolvable. // // Note that `?0` (in universe 2) must be equal to both - // `!1` and `!2`, which of course it cannot be. + // `!1_0` and `!1_1`, which of course it cannot be. for<'a, 'b> Ref<'a, Ref<'b, Ref<'a, Unit>>>: Eq< for<'c, 'd> Ref<'c, Ref<'d, Ref<'d, Unit>>>> } yields { "Unique; substitution [], lifetime constraints [ - InEnvironment { environment: Env([]), goal: '!2 == '!1 } + InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 } ]" } } @@ -1187,7 +1187,7 @@ fn normalize_under_binder() { } } } yields { - "Unique; substitution [?0 := Ref<'!1, I32>], lifetime constraints []" + "Unique; substitution [?0 := Ref<'!1_0, I32>], lifetime constraints []" } goal { @@ -1199,7 +1199,7 @@ fn normalize_under_binder() { } yields { "Unique; for { \ substitution [?0 := Ref<'?0, I32>], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \ }" } } @@ -1212,7 +1212,7 @@ fn unify_quantified_lifetimes() { } // Check that `'a` (here, `'?0`) is not unified - // with `'!1`, because they belong to incompatible + // with `'!1_0`, because they belong to incompatible // universes. goal { exists<'a> { @@ -1223,7 +1223,7 @@ fn unify_quantified_lifetimes() { } yields { "Unique; for { \ substitution [?0 := '?0], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \ }" } @@ -1239,8 +1239,8 @@ fn unify_quantified_lifetimes() { } } yields { "Unique; for { \ - substitution [?0 := '?0, ?1 := '!1], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1 }] \ + substitution [?0 := '?0, ?1 := '!1_0], \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \ }" } } @@ -1254,7 +1254,7 @@ fn equality_binder() { } // Check that `'a` (here, `'?0`) is not unified - // with `'!1`, because they belong to incompatible + // with `'!1_0`, because they belong to incompatible // universes. goal { forall { @@ -1265,7 +1265,7 @@ fn equality_binder() { } yields { "Unique; for { \ substitution [?0 := '?0], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '!2 == '?0 }] \ + lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '?0 }] \ }" } } @@ -2172,8 +2172,8 @@ fn overflow_universe() { trait Bar { } // When asked to solve X: Bar, we will produce a - // requirement to solve !1: Bar. And then when asked to - // solve that, we'll produce a requirement to solve !2: + // requirement to solve !1_0: Bar. And then when asked to + // solve that, we'll produce a requirement to solve !1_1: // Bar. And so forth. forall { X: Bar if forall { Y: Bar } } } @@ -2183,7 +2183,7 @@ fn overflow_universe() { } yields { // The internal universe canonicalization in the on-demand/recursive // solver means that when we are asked to solve (e.g.) - // `!2: Bar`, we rewrite that to `!1: Bar`, identifying a + // `!1_1: Bar`, we rewrite that to `!1_0: Bar`, identifying a // cycle. "No possible solution" } @@ -2270,9 +2270,9 @@ fn gat_unify_with_implied_wc() { // // The problem was that we wound up enumerating a goal like // -// ::Item = !1 +// ::Item = !1_0 // -// which meant "find me the types that normalize to `!1`". We had no +// which meant "find me the types that normalize to `!1_0`". We had no // problem finding these types, but after the first such type, we had // the only unique answer we would ever find, and we wanted to reach // the point where we could say "no more answers", so we kept @@ -2396,7 +2396,7 @@ fn quantified_types() { } yields { // Lifetime constraints are unsatisfiable "Unique; substitution [], \ - lifetime constraints [InEnvironment { environment: Env([]), goal: '!2 == '!1 }]" + lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '!1_0 }]" } } } diff --git a/src/test/slg.rs b/src/test/slg.rs index 7a178c292ca..b5d90cfe612 100644 --- a/src/test/slg.rs +++ b/src/test/slg.rs @@ -482,7 +482,7 @@ fn subgoal_cycle_uninhabited() { Answer { subst: Canonical { value: ConstrainedSubst { - subst: [?0 := !1], + subst: [?0 := !1_0], constraints: [] }, binders: [] @@ -550,7 +550,7 @@ fn basic_region_constraint_from_positive_impl() { constraints: [ InEnvironment { environment: Env([]), - goal: '!2 == '!1 + goal: '!1_1 == '!1_0 } ] },