From b276130eda932481aa5d6c987ff8c3775e7514a2 Mon Sep 17 00:00:00 2001 From: Jack Huey Date: Sat, 3 Oct 2020 14:55:14 -0400 Subject: [PATCH] Add static lifetime --- chalk-engine/src/slg/aggregate.rs | 13 +--- chalk-engine/src/slg/resolvent.rs | 7 +- chalk-integration/src/lowering.rs | 4 ++ chalk-ir/src/debug.rs | 1 + chalk-ir/src/fold.rs | 1 + chalk-ir/src/lib.rs | 3 + chalk-ir/src/visit.rs | 1 + chalk-parse/src/ast.rs | 1 + chalk-parse/src/parser.lalrpop | 1 + chalk-solve/src/display/ty.rs | 1 + chalk-solve/src/infer/unify.rs | 14 +++- tests/test/existential_types.rs | 112 +++++++++++++++--------------- tests/test/misc.rs | 4 +- tests/test/mod.rs | 1 + tests/test/statics.rs | 72 +++++++++++++++++++ 15 files changed, 164 insertions(+), 72 deletions(-) create mode 100644 tests/test/statics.rs diff --git a/chalk-engine/src/slg/aggregate.rs b/chalk-engine/src/slg/aggregate.rs index 09b4f6d079d..a679d7fd8ab 100644 --- a/chalk-engine/src/slg/aggregate.rs +++ b/chalk-engine/src/slg/aggregate.rs @@ -422,23 +422,14 @@ impl AntiUnifier<'_, '_, I> { fn aggregate_lifetimes(&mut self, l1: &Lifetime, l2: &Lifetime) -> Lifetime { let interner = self.interner; match (l1.data(interner), l2.data(interner)) { - (LifetimeData::InferenceVar(_), _) | (_, LifetimeData::InferenceVar(_)) => { - self.new_lifetime_variable() - } - - (LifetimeData::BoundVar(_), _) | (_, LifetimeData::BoundVar(_)) => { - self.new_lifetime_variable() - } - - (LifetimeData::Placeholder(_), LifetimeData::Placeholder(_)) => { + (LifetimeData::Phantom(..), _) | (_, LifetimeData::Phantom(..)) => unreachable!(), + _ => { if l1 == l2 { l1.clone() } else { self.new_lifetime_variable() } } - - (LifetimeData::Phantom(..), _) | (_, LifetimeData::Phantom(..)) => unreachable!(), } } diff --git a/chalk-engine/src/slg/resolvent.rs b/chalk-engine/src/slg/resolvent.rs index 2313f519d93..27e6d99913c 100644 --- a/chalk-engine/src/slg/resolvent.rs +++ b/chalk-engine/src/slg/resolvent.rs @@ -445,7 +445,8 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> { self.assert_matching_vars(*answer_depth, *pending_depth) } - (LifetimeData::Placeholder(_), LifetimeData::Placeholder(_)) => { + (LifetimeData::Static, LifetimeData::Static) + | (LifetimeData::Placeholder(_), LifetimeData::Placeholder(_)) => { assert_eq!(answer, pending); Ok(()) } @@ -455,7 +456,9 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> { answer, pending, ), - (LifetimeData::BoundVar(_), _) | (LifetimeData::Placeholder(_), _) => panic!( + (LifetimeData::Static, _) + | (LifetimeData::BoundVar(_), _) + | (LifetimeData::Placeholder(_), _) => panic!( "structural mismatch between answer `{:?}` and pending goal `{:?}`", answer, pending, ), diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 063a2868e5f..9594a6f3d05 100644 --- a/chalk-integration/src/lowering.rs +++ b/chalk-integration/src/lowering.rs @@ -910,6 +910,10 @@ impl LowerWithEnv for Lifetime { } }) } + Lifetime::Static => Ok(chalk_ir::Lifetime::new( + interner, + chalk_ir::LifetimeData::Static, + )), } } } diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index b4ed88790e4..b06e64717e8 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -285,6 +285,7 @@ impl Debug for LifetimeData { LifetimeData::BoundVar(db) => write!(fmt, "'{:?}", db), LifetimeData::InferenceVar(var) => write!(fmt, "'{:?}", var), LifetimeData::Placeholder(index) => write!(fmt, "'{:?}", index), + LifetimeData::Static => write!(fmt, "'static"), LifetimeData::Phantom(..) => unreachable!(), } } diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs index 40f5f276da1..53b10e2d3a9 100644 --- a/chalk-ir/src/fold.rs +++ b/chalk-ir/src/fold.rs @@ -489,6 +489,7 @@ where LifetimeData::Placeholder(universe) => { folder.fold_free_placeholder_lifetime(*universe, outer_binder) } + LifetimeData::Static => Ok(LifetimeData::::Static.intern(folder.target_interner())), LifetimeData::Phantom(..) => unreachable!(), } } diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs index eaf328ee7ea..85ac5592a8a 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -1064,6 +1064,7 @@ impl Lifetime { LifetimeData::BoundVar(_) => true, LifetimeData::InferenceVar(_) => false, LifetimeData::Placeholder(_) => false, + LifetimeData::Static => false, LifetimeData::Phantom(..) => unreachable!(), } } @@ -1078,6 +1079,8 @@ pub enum LifetimeData { InferenceVar(InferenceVar), /// Lifetime on some yet-unknown placeholder. Placeholder(PlaceholderIndex), + /// Static lifetime + Static, /// Lifetime on phantom data. Phantom(Void, PhantomData), } diff --git a/chalk-ir/src/visit.rs b/chalk-ir/src/visit.rs index 7612807dd6f..3dd85488b03 100644 --- a/chalk-ir/src/visit.rs +++ b/chalk-ir/src/visit.rs @@ -325,6 +325,7 @@ impl SuperVisit for Lifetime { LifetimeData::Placeholder(universe) => { visitor.visit_free_placeholder(*universe, outer_binder) } + LifetimeData::Static => R::new(), LifetimeData::Phantom(..) => unreachable!(), } } diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 3734d0e6bff..8d8e2dac72c 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -369,6 +369,7 @@ impl Default for Safety { #[derive(Clone, PartialEq, Eq, Debug)] pub enum Lifetime { Id { name: Identifier }, + Static, } #[derive(Clone, PartialEq, Eq, Debug)] diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 3aca74a0a2d..af044c66340 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -431,6 +431,7 @@ RawMutability: Mutability = { Lifetime: Lifetime = { => Lifetime::Id { name: n }, + "'static" => Lifetime::Static, }; ConstWithoutId: Const = { diff --git a/chalk-solve/src/display/ty.rs b/chalk-solve/src/display/ty.rs index e965a0213e3..c9da96081e8 100644 --- a/chalk-solve/src/display/ty.rs +++ b/chalk-solve/src/display/ty.rs @@ -274,6 +274,7 @@ impl RenderAsRust for LifetimeData { LifetimeData::Placeholder(ix) => { write!(f, "'_placeholder_{}_{}", ix.ui.counter, ix.idx) } + LifetimeData::Static => write!(f, "'static"), // Matching the void ensures at compile time that this code is // unreachable LifetimeData::Phantom(void, _) => match *void {}, diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs index 46648c5ac8f..3737c93050b 100644 --- a/chalk-solve/src/infer/unify.rs +++ b/chalk-solve/src/infer/unify.rs @@ -333,7 +333,19 @@ impl<'t, I: Interner> Unifier<'t, I> { self.unify_lifetime_var(a, b, b_var, a, a_idx.ui) } - (&LifetimeData::Placeholder(_), &LifetimeData::Placeholder(_)) => { + (&LifetimeData::InferenceVar(a_var), &LifetimeData::Static) => { + self.unify_lifetime_var(a, b, a_var, b, UniverseIndex::root()) + } + + (&LifetimeData::Static, &LifetimeData::InferenceVar(b_var)) => { + self.unify_lifetime_var(a, b, b_var, a, UniverseIndex::root()) + } + + (&LifetimeData::Static, &LifetimeData::Static) => Ok(()), + + (&LifetimeData::Static, &LifetimeData::Placeholder(_)) + | (&LifetimeData::Placeholder(_), &LifetimeData::Static) + | (&LifetimeData::Placeholder(_), &LifetimeData::Placeholder(_)) => { if a != b { Ok(self.push_lifetime_eq_goals(a.clone(), b.clone())) } else { diff --git a/tests/test/existential_types.rs b/tests/test/existential_types.rs index 0faa659a3cf..38615cd90a6 100644 --- a/tests/test/existential_types.rs +++ b/tests/test/existential_types.rs @@ -10,8 +10,8 @@ fn dyn_Clone_is_Clone() { } goal { - forall<'static> { - dyn Clone + 'static: Clone + forall<'s> { + dyn Clone + 's: Clone } } yields { "Unique; substitution []" @@ -28,8 +28,8 @@ fn dyn_Clone_is_not_Send() { } goal { - forall<'static> { - dyn Clone + 'static: Send + forall<'s> { + dyn Clone + 's: Send } } yields { "No possible solution" @@ -46,8 +46,8 @@ fn dyn_Clone_Send_is_Send() { } goal { - forall<'static> { - (dyn Clone + Send + 'static): Send + forall<'s> { + (dyn Clone + Send + 's): Send } } yields { "Unique; substitution []" @@ -66,17 +66,17 @@ fn dyn_Foo_Bar() { } goal { - forall<'static> { - dyn Foo + 'static: Foo + forall<'s> { + dyn Foo + 's: Foo } } yields { "No possible solution" } goal { - forall<'static> { + forall<'s> { exists { - dyn Foo + 'static: Foo + dyn Foo + 's: Foo } } } yields { @@ -97,33 +97,33 @@ fn dyn_super_trait_simple() { } goal { - forall<'static> { - dyn Bar + 'static: Bar + forall<'s> { + dyn Bar + 's: Bar } } yields { "Unique" } goal { - forall<'static> { - dyn Bar + 'static: Foo + forall<'s> { + dyn Bar + 's: Foo } } yields { "Unique" } goal { - forall<'static> { - dyn Bar + 'static: Foo + forall<'s> { + dyn Bar + 's: Foo } } yields { "No possible solution" } goal { - forall<'static> { + forall<'s> { exists { - dyn Bar + 'static: Foo + dyn Bar + 's: Foo } } } yields { @@ -146,8 +146,8 @@ fn dyn_super_trait_cycle() { // We currently can't prove this because of the cyclic where clauses. // But importantly, we don't crash or get into an infinite loop. goal { - forall<'static> { - dyn Bar + 'static: Bar + forall<'s> { + dyn Bar + 's: Bar } } yields { "No possible solution" @@ -168,24 +168,24 @@ fn dyn_super_trait_not_a_cycle() { } goal { - forall<'static> { - dyn Bar + 'static: Foo + forall<'s> { + dyn Bar + 's: Foo } } yields { "Unique" } goal { - forall<'static> { - dyn Bar + 'static: Thing + forall<'s> { + dyn Bar + 's: Thing } } yields { "Unique" } goal { - forall<'static> { - dyn Bar + 'static: Thing + forall<'s> { + dyn Bar + 's: Thing } } yields { "Unique" @@ -206,9 +206,9 @@ fn dyn_super_trait_higher_ranked() { } goal { - forall<'static> { + forall<'s> { forall<'x> { - dyn Baz + 'static: Bar<'x> + dyn Baz + 's: Bar<'x> } } } yields { @@ -216,9 +216,9 @@ fn dyn_super_trait_higher_ranked() { } goal { - forall<'static> { + forall<'s> { forall<'x> { - dyn Baz + 'static: Foo<'x> + dyn Baz + 's: Foo<'x> } } } yields { @@ -226,8 +226,8 @@ fn dyn_super_trait_higher_ranked() { } goal { - forall<'x, 'y, 'static> { - dyn Bar<'y> + 'static: Foo<'x> + forall<'x, 'y, 's> { + dyn Bar<'y> + 's: Foo<'x> } } yields { "Unique" @@ -247,16 +247,16 @@ fn dyn_super_trait_non_super_trait_clause() { } goal { - forall<'static> { - dyn Foo + 'static: Foo + forall<'s> { + dyn Foo + 's: Foo } } yields { "Unique" } goal { - forall<'static> { - dyn Foo + 'static: Bar + forall<'s> { + dyn Foo + 's: Bar } } yields { "No possible solution" @@ -275,37 +275,37 @@ fn dyn_higher_ranked_type_arguments() { } goal { - forall<'static> { - dyn forall<'a> Foo> + 'static: Foo> + forall<'s> { + dyn forall<'a> Foo> + 's: Foo> } } yields { "Unique; substitution [], lifetime constraints []" } goal { - forall<'static> { - dyn forall<'a> Foo> + Bar + 'static: Foo> + forall<'s> { + dyn forall<'a> Foo> + Bar + 's: Foo> } } yields { "Unique; substitution [], lifetime constraints []" } goal { - forall<'static> { - dyn forall<'a> Foo> + Bar + 'static: Bar + forall<'s> { + dyn forall<'a> Foo> + Bar + 's: Bar } } yields { "Unique; substitution [], lifetime constraints []" } goal { - forall<'static> { + forall<'s> { forall<'a> { - dyn Foo> + 'static: Foo> + dyn Foo> + 's: Foo> } } } yields { - // Note that this requires 'a == 'static, so it would be resolveable later on. + // Note that this requires 'a == 's, so it would be resolveable later on. "Unique; substitution [], lifetime constraints [\ InEnvironment { environment: Env([]), goal: '!1_0: '!2_0 }, \ InEnvironment { environment: Env([]), goal: '!2_0: '!1_0 }\ @@ -330,9 +330,9 @@ fn dyn_binders_reverse() { // Note: these constraints are ultimately unresolveable (we // have to show that 'a == 'b, basically) goal { - forall<'static> { - dyn forall<'a, 'b> Fn> + 'static: Eq< - dyn forall<'c> Fn> + 'static + forall<'s> { + dyn forall<'a, 'b> Fn> + 's: Eq< + dyn forall<'c> Fn> + 's > } } yields { @@ -347,9 +347,9 @@ fn dyn_binders_reverse() { // Note: these constraints are ultimately unresolveable (we // have to show that 'a == 'b, basically) goal { - forall<'static> { - dyn forall<'c> Fn> + 'static: Eq< - dyn forall<'a, 'b> Fn> + 'static + forall<'s> { + dyn forall<'c> Fn> + 's: Eq< + dyn forall<'a, 'b> Fn> + 's > } } yields { @@ -363,9 +363,9 @@ fn dyn_binders_reverse() { // Note: ordering of parameters is reversed here, but that's no problem goal { - forall<'static> { - dyn forall<'c, 'd> Fn> + 'static: Eq< - dyn forall<'a, 'b> Fn> + 'static + forall<'s> { + dyn forall<'c, 'd> Fn> + 's: Eq< + dyn forall<'a, 'b> Fn> + 's > } } yields { @@ -409,8 +409,8 @@ fn dyn_associated_type_binding() { goal { exists { - forall<'static> { - + 'static as FnOnce<()>>::Output = T + forall<'s> { + + 's as FnOnce<()>>::Output = T } } } yields[SolverChoice::recursive()] { diff --git a/tests/test/misc.rs b/tests/test/misc.rs index 23ddd2591ad..66d42b5cd9e 100644 --- a/tests/test/misc.rs +++ b/tests/test/misc.rs @@ -746,8 +746,8 @@ fn empty_definite_guidance() { } goal { - forall<'static> { - A: OtherTrait<'static> + forall<'a> { + A: OtherTrait<'a> } // the program fails coherence, so which answer we get here exactly // isn't that important -- this is mainly a regression test for a diff --git a/tests/test/mod.rs b/tests/test/mod.rs index e8bcdb55c6d..e4222fd4125 100644 --- a/tests/test/mod.rs +++ b/tests/test/mod.rs @@ -344,6 +344,7 @@ mod projection; mod refs; mod scalars; mod slices; +mod statics; mod string; mod tuples; mod unify; diff --git a/tests/test/statics.rs b/tests/test/statics.rs new file mode 100644 index 00000000000..5ca9430be2f --- /dev/null +++ b/tests/test/statics.rs @@ -0,0 +1,72 @@ +//! Tests for the static lifetime + +use super::*; + + +#[test] +fn static_lowering() { + lowering_success! { + program { + struct A<'a> where 'a: 'static {} + trait A<'a> where 'a: 'static {} + fn foo(a: &'static ()); + } + } +} + +#[test] +fn static_outlives() { + test! { + program { + trait Foo<'a> where 'a: 'static {} + struct Bar {} + + impl<'a> Foo<'a> for Bar where 'a: 'static {} + } + + goal { + exists<'a> { + Bar: Foo<'a> + } + } yields { + "Unique; for { substitution [?0 := '^0.0], lifetime constraints [InEnvironment { environment: Env([]), goal: '^0.0: 'static }] }" + } + + goal { + forall<'a> { + Bar: Foo<'a> + } + } yields { + "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: 'static }]" + } + } +} + +#[test] +fn static_impls() { + test! { + program { + struct Foo {} + trait Bar {} + impl<'a> Bar for &'a Foo {} + } + + goal { + &'static Foo: Bar + } yields { + "Unique; substitution [], lifetime constraints []" + } + + goal { + forall<'a> { &'a Foo: Bar } + } yields { + "Unique; substitution [], lifetime constraints []" + } + + goal { + exists<'a> { &'a Foo: Bar } + } yields { + "Unique; for { substitution [?0 := '^0.0], lifetime constraints [] }" + } + } +}