Skip to content

Commit cf0b0db

Browse files
jackh726jackh726
authored
Merge pull request #419 from nikomatsakis/outlives-not-equality
convert from lifetime equality constraints to outlives constraints
2 parents 15daa1a + a120069 commit cf0b0db

File tree

8 files changed

+76
-20
lines changed

8 files changed

+76
-20
lines changed

‎chalk-ir/src/debug.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -725,7 +725,7 @@ impl<T: Debug, L: Debug> Debug for ParameterKind<T, L> {
725725
impl<I: Interner> Debug for Constraint<I> {
726726
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
727727
match self {
728-
Constraint::LifetimeEq(a, b) => write!(fmt, "{:?} == {:?}", a, b),
728+
Constraint::Outlives(a, b) => write!(fmt, "{:?}: {:?}", a, b),
729729
}
730730
}
731731
}

‎chalk-ir/src/lib.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1909,7 +1909,7 @@ pub enum QuantifierKind {
19091909
/// checking in the compiler.
19101910
#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)]
19111911
pub enum Constraint<I: Interner> {
1912-
LifetimeEq(Lifetime<I>, Lifetime<I>),
1912+
Outlives(Lifetime<I>, Lifetime<I>),
19131913
}
19141914

19151915
/// A mapping of inference variables to instantiations thereof.

‎chalk-solve/src/infer/test.rs‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -303,9 +303,13 @@ fn lifetime_constraint_indirect() {
303303
let UnificationResult { goals, constraints } =
304304
table.unify(interner, &environment0, &t_c, &t_b).unwrap();
305305
assert!(goals.is_empty());
306-
assert_eq!(constraints.len(), 1);
306+
assert_eq!(constraints.len(), 2);
307307
assert_eq!(
308308
format!("{:?}", constraints[0]),
309-
"InEnvironment { environment: Env([]), goal: \'?2 == \'!1_0 }",
309+
"InEnvironment { environment: Env([]), goal: \'?2: \'!1_0 }",
310+
);
311+
assert_eq!(
312+
format!("{:?}", constraints[1]),
313+
"InEnvironment { environment: Env([]), goal: \'!1_0: \'?2 }",
310314
);
311315
}

‎chalk-solve/src/infer/unify.rs‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -337,7 +337,11 @@ impl<'t, I: Interner> Unifier<'t, I> {
337337
fn push_lifetime_eq_constraint(&mut self, a: Lifetime<I>, b: Lifetime<I>) {
338338
self.constraints.push(InEnvironment::new(
339339
self.environment,
340-
Constraint::LifetimeEq(a, b),
340+
Constraint::Outlives(a.clone(), b.clone()),
341+
));
342+
self.constraints.push(InEnvironment::new(
343+
self.environment,
344+
Constraint::Outlives(b, a),
341345
));
342346
}
343347
}

‎tests/test/existential_types.rs‎

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,10 @@ fn dyn_higher_ranked_type_arguments() {
161161
}
162162
} yields {
163163
// Note that this requires 'a == 'static, so it would be resolveable later on.
164-
"Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '!1_0 }]"
164+
"Unique; substitution [], lifetime constraints [\
165+
InEnvironment { environment: Env([]), goal: '!1_0: '!2_0 }, \
166+
InEnvironment { environment: Env([]), goal: '!2_0: '!1_0 }\
167+
]"
165168
}
166169
}
167170
}
@@ -186,7 +189,12 @@ fn dyn_binders_reverse() {
186189
dyn forall<'c> Fn<Refs<'c, 'c>>
187190
>
188191
} yields {
189-
"Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!3_0 == '!3_1 }, InEnvironment { environment: Env([]), goal: '!6_0 == '!6_1 }]"
192+
"Unique; substitution [], lifetime constraints [\
193+
InEnvironment { environment: Env([]), goal: '!3_0: '!3_1 }, \
194+
InEnvironment { environment: Env([]), goal: '!3_1: '!3_0 }, \
195+
InEnvironment { environment: Env([]), goal: '!6_0: '!6_1 }, \
196+
InEnvironment { environment: Env([]), goal: '!6_1: '!6_0 }\
197+
]"
190198
}
191199

192200
// Note: these constraints are ultimately unresolveable (we
@@ -196,7 +204,12 @@ fn dyn_binders_reverse() {
196204
dyn forall<'a, 'b> Fn<Refs<'a, 'b>>
197205
>
198206
} yields {
199-
"Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_1 == '!2_0 }, InEnvironment { environment: Env([]), goal: '!5_1 == '!5_0 }]"
207+
"Unique; substitution [], lifetime constraints [\
208+
InEnvironment { environment: Env([]), goal: '!2_0: '!2_1 }, \
209+
InEnvironment { environment: Env([]), goal: '!2_1: '!2_0 }, \
210+
InEnvironment { environment: Env([]), goal: '!5_0: '!5_1 }, \
211+
InEnvironment { environment: Env([]), goal: '!5_1: '!5_0 }\
212+
]"
200213
}
201214

202215
// Note: ordering of parameters is reversed here, but that's no problem

‎tests/test/misc.rs‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,10 @@ fn basic_region_constraint_from_positive_impl() {
256256
goal {
257257
forall<'a, 'b, T> { Ref<'a, 'b, T>: Foo }
258258
} yields_all[SolverChoice::slg(3, None)] {
259-
"substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }]"
259+
"substitution [], lifetime constraints [\
260+
InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }, \
261+
InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }\
262+
]"
260263
}
261264
}
262265
}

‎tests/test/projection.rs‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -724,7 +724,9 @@ fn normalize_under_binder() {
724724
} yields {
725725
"Unique; for<?U0> { \
726726
substitution [?0 := Ref<'^0.0, I32>], \
727-
lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
727+
lifetime constraints [\
728+
InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }, \
729+
InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }] \
728730
}"
729731
}
730732
}
@@ -754,7 +756,11 @@ fn normalize_under_binder_multi() {
754756
}
755757
} yields_all {
756758
"substitution [?0 := I32], lifetime constraints []",
757-
"for<?U0,?U0> { substitution [?0 := (Deref::Item)<Ref<'^0.0, I32>, '^0.1>], lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }, InEnvironment { environment: Env([]), goal: '^0.1 == '!1_0 }] }"
759+
"for<?U0,?U0> { substitution [?0 := (Deref::Item)<Ref<'^0.0, I32>, '^0.1>], lifetime constraints [\
760+
InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }, \
761+
InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }, \
762+
InEnvironment { environment: Env([]), goal: '^0.1: '!1_0 }, \
763+
InEnvironment { environment: Env([]), goal: '!1_0: '^0.1 }] }"
758764
}
759765

760766
goal {

‎tests/test/unify.rs‎

Lines changed: 35 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,8 @@ fn region_equality() {
2323
} yields {
2424
"Unique; substitution [],
2525
lifetime constraints \
26-
[InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }]
26+
[InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, \
27+
InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }]
2728
"
2829
}
2930

@@ -71,7 +72,11 @@ fn forall_equality() {
7172
for<'a, 'b> fn(Ref<'a, Ref<'b, Ref<'a, Unit>>>): Eq<
7273
for<'c, 'd> fn(Ref<'c, Ref<'d, Ref<'d, Unit>>>)>
7374
} yields {
74-
"Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }, InEnvironment { environment: Env([]), goal: '!2_1 == '!2_0 }]"
75+
"Unique; substitution [], lifetime constraints [\
76+
InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, \
77+
InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }, \
78+
InEnvironment { environment: Env([]), goal: '!2_0: '!2_1 }, \
79+
InEnvironment { environment: Env([]), goal: '!2_1: '!2_0 }]"
7580
}
7681
}
7782
}
@@ -94,7 +99,10 @@ fn unify_quantified_lifetimes() {
9499
} yields {
95100
"Unique; for<?U0> { \
96101
substitution [?0 := '^0.0], \
97-
lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
102+
lifetime constraints [\
103+
InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }, \
104+
InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }\
105+
] \
98106
}"
99107
}
100108

@@ -111,13 +119,19 @@ fn unify_quantified_lifetimes() {
111119
} yields[SolverChoice::slg(10, None)] {
112120
"Unique; for<?U0> { \
113121
substitution [?0 := '^0.0, ?1 := '!1_0], \
114-
lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
122+
lifetime constraints [\
123+
InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }, \
124+
InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }\
125+
] \
115126
}"
116127
} yields[SolverChoice::recursive()] {
117128
// only difference is in the value of ?1, which is equivalent
118129
"Unique; for<?U0> { \
119130
substitution [?0 := '^0.0, ?1 := '^0.0], \
120-
lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0 == '!1_0 }] \
131+
lifetime constraints [\
132+
InEnvironment { environment: Env([]), goal: '!1_0: '^0.0 }, \
133+
InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }\
134+
] \
121135
}"
122136
}
123137
}
@@ -142,7 +156,10 @@ fn equality_binder() {
142156
} yields {
143157
"Unique; for<?U1> { \
144158
substitution [?0 := '^0.0], \
145-
lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '^0.0 }] \
159+
lifetime constraints [\
160+
InEnvironment { environment: Env([]), goal: '!2_0: '^0.0 }, \
161+
InEnvironment { environment: Env([]), goal: '^0.0: '!2_0 }\
162+
] \
146163
}"
147164
}
148165
}
@@ -158,13 +175,19 @@ fn equality_binder2() {
158175
goal {
159176
for<'b, 'c> fn(Ref<'b, 'c>) = for<'a> fn(Ref<'a, 'a>)
160177
} yields {
161-
"Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }]"
178+
"Unique; substitution [], lifetime constraints [\
179+
InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, \
180+
InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }\
181+
]"
162182
}
163183

164184
goal {
165185
for<'a> fn(Ref<'a, 'a>) = for<'b, 'c> fn(Ref<'b, 'c>)
166186
} yields {
167-
"Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '!2_1 }]"
187+
"Unique; substitution [], lifetime constraints [\
188+
InEnvironment { environment: Env([]), goal: '!2_0: '!2_1 }, \
189+
InEnvironment { environment: Env([]), goal: '!2_1: '!2_0 }\
190+
]"
168191
}
169192
}
170193
}
@@ -303,7 +326,10 @@ fn quantified_types() {
303326
} yields {
304327
// Lifetime constraints are unsatisfiable
305328
"Unique; substitution [], \
306-
lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0 == '!3_0 }]"
329+
lifetime constraints [\
330+
InEnvironment { environment: Env([]), goal: '!1_0: '!3_0 }, \
331+
InEnvironment { environment: Env([]), goal: '!3_0: '!1_0 }\
332+
]"
307333
}
308334
}
309335
}

0 commit comments

Comments
 (0)