From b2604d4173346c8dfdb0336813def5e36220f11e Mon Sep 17 00:00:00 2001 From: Waffle Lapkin Date: Thu, 2 Jan 2025 14:11:40 +0100 Subject: [PATCH 1/7] Make a comment more clear The rest of the code uses A/B, so use them here too. --- chalk-solve/src/clauses/builtin_traits/unsize.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chalk-solve/src/clauses/builtin_traits/unsize.rs b/chalk-solve/src/clauses/builtin_traits/unsize.rs index 6682735b692..0a8c0a0a3c3 100644 --- a/chalk-solve/src/clauses/builtin_traits/unsize.rs +++ b/chalk-solve/src/clauses/builtin_traits/unsize.rs @@ -190,7 +190,7 @@ pub fn add_unsize_program_clauses( // `fn confirm_builtin_unisize_candidate` in rustc. match (source_ty.kind(interner), target_ty.kind(interner)) { - // dyn Trait + AutoX + 'a -> dyn Trait + AutoY + 'b + // dyn TraitA + AutoA + 'a -> dyn TraitB + AutoB + 'b ( TyKind::Dyn(DynTy { bounds: bounds_a, From f5da4bbff2089a4bb5d41846b227cb099db725ec Mon Sep 17 00:00:00 2001 From: Waffle Lapkin Date: Thu, 2 Jan 2025 16:21:25 +0100 Subject: [PATCH 2/7] fix comment typo --- chalk-solve/src/clauses/builtin_traits/unsize.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chalk-solve/src/clauses/builtin_traits/unsize.rs b/chalk-solve/src/clauses/builtin_traits/unsize.rs index 0a8c0a0a3c3..13e55cbd291 100644 --- a/chalk-solve/src/clauses/builtin_traits/unsize.rs +++ b/chalk-solve/src/clauses/builtin_traits/unsize.rs @@ -187,7 +187,7 @@ pub fn add_unsize_program_clauses( // could be lifted. // // for more info visit `fn assemble_candidates_for_unsizing` and - // `fn confirm_builtin_unisize_candidate` in rustc. + // `fn confirm_builtin_unsize_candidate` in rustc. match (source_ty.kind(interner), target_ty.kind(interner)) { // dyn TraitA + AutoA + 'a -> dyn TraitB + AutoB + 'b From 3ed9dc24c9e0b09aa781ec0a311b74f97767c111 Mon Sep 17 00:00:00 2001 From: Waffle Lapkin Date: Thu, 2 Jan 2025 14:12:48 +0100 Subject: [PATCH 3/7] Allow unsizing `dyn Trait -> dyn Trait + Auto` if `Trait: Auto` --- .../src/clauses/builtin_traits/unsize.rs | 56 ++++++++++++++----- chalk-solve/src/clauses/super_traits.rs | 2 +- tests/test/unsize.rs | 37 ++++++++++++ 3 files changed, 81 insertions(+), 14 deletions(-) diff --git a/chalk-solve/src/clauses/builtin_traits/unsize.rs b/chalk-solve/src/clauses/builtin_traits/unsize.rs index 13e55cbd291..60a19d56759 100644 --- a/chalk-solve/src/clauses/builtin_traits/unsize.rs +++ b/chalk-solve/src/clauses/builtin_traits/unsize.rs @@ -2,6 +2,7 @@ use std::collections::HashSet; use std::iter; use std::ops::ControlFlow; +use crate::clauses::super_traits::super_traits; use crate::clauses::ClauseBuilder; use crate::rust_ir::AdtKind; use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait}; @@ -204,7 +205,20 @@ pub fn add_unsize_program_clauses( let principal_a = principal_id(db, bounds_a); let principal_b = principal_id(db, bounds_b); - let auto_trait_ids_a: Vec<_> = auto_trait_ids(db, bounds_a).collect(); + // Include super traits in a list of auto traits for A, + // to allow `dyn Trait -> dyn Trait + X` if `Trait: X`. + let auto_trait_ids_a: Vec<_> = auto_trait_ids(db, bounds_a) + .chain(principal_a.into_iter().flat_map(|principal_a| { + super_traits(db, principal_a) + .into_value_and_skipped_binders() + .0 + .0 + .into_iter() + .map(|x| x.skip_binders().trait_id) + .filter(|&x| db.trait_datum(x).is_auto_trait()) + })) + .collect(); + let auto_trait_ids_b: Vec<_> = auto_trait_ids(db, bounds_b).collect(); let may_apply = principal_a == principal_b @@ -234,7 +248,7 @@ pub fn add_unsize_program_clauses( // ------------------ // Construct a new trait object type by taking the source ty, - // filtering out auto traits of source that are not present in target + // replacing auto traits of source with those of target, // and changing source lifetime to target lifetime. // // In order for the coercion to be valid, this new type @@ -243,17 +257,33 @@ pub fn add_unsize_program_clauses( bounds: bounds_a.map_ref(|bounds| { QuantifiedWhereClauses::from_iter( interner, - bounds.iter(interner).filter(|bound| { - let trait_id = match bound.trait_id() { - Some(id) => id, - None => return true, - }; - - if auto_trait_ids_a.iter().all(|&id_a| id_a != trait_id) { - return true; - } - auto_trait_ids_b.iter().any(|&id_b| id_b == trait_id) - }), + bounds + .iter(interner) + .cloned() + .filter_map(|bound| { + let Some(trait_id) = bound.trait_id() else { + // Keep non-"implements" bounds as-is + return Some(bound); + }; + + // Auto traits are already checked above, ignore them + // (we'll use the ones from B below) + if db.trait_datum(trait_id).is_auto_trait() { + return None; + } + + // The only "implements" bound that is not an auto trait, is the principal + assert_eq!(Some(trait_id), principal_a); + Some(bound) + }) + // Add auto traits from B (again, they are already checked above). + .chain(bounds_b.skip_binders().iter(interner).cloned().filter( + |bound| { + bound.trait_id().is_some_and(|trait_id| { + db.trait_datum(trait_id).is_auto_trait() + }) + }, + )), ) }), lifetime: lifetime_b.clone(), diff --git a/chalk-solve/src/clauses/super_traits.rs b/chalk-solve/src/clauses/super_traits.rs index c6040b6dc28..eeb3678ce8d 100644 --- a/chalk-solve/src/clauses/super_traits.rs +++ b/chalk-solve/src/clauses/super_traits.rs @@ -73,7 +73,7 @@ pub(super) fn push_trait_super_clauses( } } -fn super_traits( +pub(crate) fn super_traits( db: &dyn RustIrDatabase, trait_id: TraitId, ) -> Binders<( diff --git a/tests/test/unsize.rs b/tests/test/unsize.rs index 21dd0c62ef9..fe0c99c8f9d 100644 --- a/tests/test/unsize.rs +++ b/tests/test/unsize.rs @@ -142,6 +142,43 @@ fn dyn_to_dyn_unsizing() { } } +#[test] +fn super_auto_trait() { + test! { + program { + #[lang(unsize)] + trait Unsize {} + + #[object_safe] + trait Principal where Self: SuperAuto {} + + #[auto] + #[object_safe] + trait SuperAuto {} + + #[auto] + #[object_safe] + trait Auto {} + } + + goal { + forall<'a> { + dyn Principal + 'a: Unsize + } + } yields { + expect!["Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"] + } + + goal { + forall<'a> { + dyn Principal + Auto + 'a: Unsize + } + } yields { + expect!["Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"] + } + } +} + #[test] fn ty_to_dyn_unsizing() { test! { From f7655e0138be000fb18d746d42d7e5c6e3eedaa3 Mon Sep 17 00:00:00 2001 From: Waffle Lapkin Date: Thu, 2 Jan 2025 14:08:34 +0100 Subject: [PATCH 4/7] Allowing dropping principal when unsizing `dyn Trait+A -> dyn A` --- chalk-solve/src/clauses/builtin_traits/unsize.rs | 10 ++++++++-- tests/test/unsize.rs | 2 +- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/chalk-solve/src/clauses/builtin_traits/unsize.rs b/chalk-solve/src/clauses/builtin_traits/unsize.rs index 60a19d56759..5d0846859be 100644 --- a/chalk-solve/src/clauses/builtin_traits/unsize.rs +++ b/chalk-solve/src/clauses/builtin_traits/unsize.rs @@ -221,7 +221,10 @@ pub fn add_unsize_program_clauses( let auto_trait_ids_b: Vec<_> = auto_trait_ids(db, bounds_b).collect(); - let may_apply = principal_a == principal_b + // If B has a principal, then A must as well + // (i.e. we allow dropping principal, but not creating a principal out of thin air). + // `AutoB` must be a subset of `AutoA`. + let may_apply = principal_a.is_some() >= principal_b.is_some() && auto_trait_ids_b .iter() .all(|id_b| auto_trait_ids_a.iter().any(|id_a| id_a == id_b)); @@ -274,7 +277,10 @@ pub fn add_unsize_program_clauses( // The only "implements" bound that is not an auto trait, is the principal assert_eq!(Some(trait_id), principal_a); - Some(bound) + + // Only include principal_a if the principal_b is also present + // (this allows dropping principal, `dyn Tr+A -> dyn A`) + principal_b.is_some().then(|| bound) }) // Add auto traits from B (again, they are already checked above). .chain(bounds_b.skip_binders().iter(interner).cloned().filter( diff --git a/tests/test/unsize.rs b/tests/test/unsize.rs index fe0c99c8f9d..b6cdb7c03cd 100644 --- a/tests/test/unsize.rs +++ b/tests/test/unsize.rs @@ -110,7 +110,7 @@ fn dyn_to_dyn_unsizing() { dyn Principal + Auto1 + 'a: Unsize } } yields { - expect![["No possible solution"]] + expect!["Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"] } // Non-matching principal traits From e6659628bda9961f7bf4cae0a49b7abb2b6f0b95 Mon Sep 17 00:00:00 2001 From: Waffle Lapkin Date: Thu, 2 Jan 2025 17:33:07 +0100 Subject: [PATCH 5/7] Implement trait upcasting Co-authored-by: Ryo Yoshida --- .../src/clauses/builtin_traits/unsize.rs | 228 ++++++++++++------ tests/test/unsize.rs | 94 ++++++++ 2 files changed, 254 insertions(+), 68 deletions(-) diff --git a/chalk-solve/src/clauses/builtin_traits/unsize.rs b/chalk-solve/src/clauses/builtin_traits/unsize.rs index 5d0846859be..d999a0229d7 100644 --- a/chalk-solve/src/clauses/builtin_traits/unsize.rs +++ b/chalk-solve/src/clauses/builtin_traits/unsize.rs @@ -137,17 +137,27 @@ fn uses_outer_binder_params( matches!(flow, ControlFlow::Break(_)) } -fn principal_id( +fn principal_trait_ref( db: &dyn RustIrDatabase, bounds: &Binders>, -) -> Option> { - let interner = db.interner(); - +) -> Option>>> { bounds - .skip_binders() - .iter(interner) - .filter_map(|b| b.trait_id()) - .find(|&id| !db.trait_datum(id).is_auto_trait()) + .map_ref(|b| b.iter(db.interner())) + .into_iter() + .find_map(|b| { + b.filter_map(|qwc| { + qwc.as_ref().filter_map(|wc| match wc { + WhereClause::Implemented(trait_ref) => { + if db.trait_datum(trait_ref.trait_id).is_auto_trait() { + None + } else { + Some(trait_ref.clone()) + } + } + _ => None, + }) + }) + }) } fn auto_trait_ids<'a, I: Interner>( @@ -202,8 +212,12 @@ pub fn add_unsize_program_clauses( lifetime: lifetime_b, }), ) => { - let principal_a = principal_id(db, bounds_a); - let principal_b = principal_id(db, bounds_b); + let principal_trait_ref_a = principal_trait_ref(db, bounds_a); + let principal_a = principal_trait_ref_a + .as_ref() + .map(|trait_ref| trait_ref.skip_binders().skip_binders().trait_id); + let principal_b = principal_trait_ref(db, bounds_b) + .map(|trait_ref| trait_ref.skip_binders().skip_binders().trait_id); // Include super traits in a list of auto traits for A, // to allow `dyn Trait -> dyn Trait + X` if `Trait: X`. @@ -233,6 +247,13 @@ pub fn add_unsize_program_clauses( return; } + // Check that source lifetime outlives target lifetime + let lifetime_outlives_goal: Goal = WhereClause::LifetimeOutlives(LifetimeOutlives { + a: lifetime_a.clone(), + b: lifetime_b.clone(), + }) + .cast(interner); + // COMMENT FROM RUSTC: // ------------------ // Require that the traits involved in this upcast are **equal**; @@ -250,67 +271,138 @@ pub fn add_unsize_program_clauses( // with what our behavior should be there. -nikomatsakis // ------------------ - // Construct a new trait object type by taking the source ty, - // replacing auto traits of source with those of target, - // and changing source lifetime to target lifetime. - // - // In order for the coercion to be valid, this new type - // should be equal to target type. - let new_source_ty = TyKind::Dyn(DynTy { - bounds: bounds_a.map_ref(|bounds| { - QuantifiedWhereClauses::from_iter( - interner, - bounds - .iter(interner) - .cloned() - .filter_map(|bound| { - let Some(trait_id) = bound.trait_id() else { - // Keep non-"implements" bounds as-is - return Some(bound); - }; - - // Auto traits are already checked above, ignore them - // (we'll use the ones from B below) - if db.trait_datum(trait_id).is_auto_trait() { - return None; - } - - // The only "implements" bound that is not an auto trait, is the principal - assert_eq!(Some(trait_id), principal_a); - - // Only include principal_a if the principal_b is also present - // (this allows dropping principal, `dyn Tr+A -> dyn A`) - principal_b.is_some().then(|| bound) + if principal_a == principal_b || principal_b.is_none() { + // Construct a new trait object type by taking the source ty, + // replacing auto traits of source with those of target, + // and changing source lifetime to target lifetime. + // + // In order for the coercion to be valid, this new type + // should be equal to target type. + let new_source_ty = TyKind::Dyn(DynTy { + bounds: bounds_a.map_ref(|bounds| { + QuantifiedWhereClauses::from_iter( + interner, + bounds + .iter(interner) + .cloned() + .filter_map(|bound| { + let Some(trait_id) = bound.trait_id() else { + // Keep non-"implements" bounds as-is + return Some(bound); + }; + + // Auto traits are already checked above, ignore them + // (we'll use the ones from B below) + if db.trait_datum(trait_id).is_auto_trait() { + return None; + } + + // The only "implements" bound that is not an auto trait, is the principal + assert_eq!(Some(trait_id), principal_a); + + // Only include principal_a if the principal_b is also present + // (this allows dropping principal, `dyn Tr+A -> dyn A`) + principal_b.is_some().then(|| bound) + }) + // Add auto traits from B (again, they are already checked above). + .chain(bounds_b.skip_binders().iter(interner).cloned().filter( + |bound| { + bound.trait_id().is_some_and(|trait_id| { + db.trait_datum(trait_id).is_auto_trait() + }) + }, + )), + ) + }), + lifetime: lifetime_b.clone(), + }) + .intern(interner); + + // Check that new source is equal to target + let eq_goal = EqGoal { + a: new_source_ty.cast(interner), + b: target_ty.clone().cast(interner), + } + .cast(interner); + + builder.push_clause(trait_ref, [eq_goal, lifetime_outlives_goal].iter()); + } else { + // Conditions above imply that both of these are always `Some` + // (b != None, b is Some iff a is Some). + let principal_a = principal_a.unwrap(); + let principal_b = principal_b.unwrap(); + + let principal_trait_ref_a = principal_trait_ref_a.unwrap(); + let applicable_super_traits = super_traits(db, principal_a) + .map(|(super_trait_refs, _)| super_trait_refs) + .into_iter() + .filter(|trait_ref| { + trait_ref.skip_binders().skip_binders().trait_id == principal_b + }); + + for super_trait_ref in applicable_super_traits { + // `super_trait_ref` is, at this point, quantified over generic params of + // `principal_a` and relevant higher-ranked lifetimes that come from super + // trait elaboration (see comments on `super_traits()`). + // + // So if we have `trait Trait<'a, T>: for<'b> Super<'a, 'b, T> {}`, + // `super_trait_ref` can be something like + // `for for<'b> Self: Super<'a, 'b, T>`. + // + // We need to convert it into a bound for `DynTy`. We do this by substituting + // bound vars of `principal_trait_ref_a` and then fusing inner binders for + // higher-ranked lifetimes. + let rebound_super_trait_ref = principal_trait_ref_a.map_ref(|q_trait_ref_a| { + q_trait_ref_a + .map_ref(|trait_ref_a| { + super_trait_ref.substitute(interner, &trait_ref_a.substitution) }) - // Add auto traits from B (again, they are already checked above). - .chain(bounds_b.skip_binders().iter(interner).cloned().filter( - |bound| { - bound.trait_id().is_some_and(|trait_id| { - db.trait_datum(trait_id).is_auto_trait() - }) - }, - )), - ) - }), - lifetime: lifetime_b.clone(), - }) - .intern(interner); + .fuse_binders(interner) + }); - // Check that new source is equal to target - let eq_goal = EqGoal { - a: new_source_ty.cast(interner), - b: target_ty.clone().cast(interner), - } - .cast(interner); - - // Check that source lifetime outlives target lifetime - let lifetime_outlives_goal: Goal = WhereClause::LifetimeOutlives(LifetimeOutlives { - a: lifetime_a.clone(), - b: lifetime_b.clone(), - }) - .cast(interner); + // Skip `for` binder. We'll rebind it immediately below. + let new_principal_trait_ref = rebound_super_trait_ref + .into_value_and_skipped_binders() + .0 + .map(|it| it.cast(interner)); + + // Swap trait ref for `principal_a` with the new trait ref, drop the auto + // traits not included in the upcast target. + let new_source_ty = TyKind::Dyn(DynTy { + bounds: bounds_a.map_ref(|bounds| { + QuantifiedWhereClauses::from_iter( + interner, + bounds.iter(interner).cloned().filter_map(|bound| { + let trait_id = match bound.trait_id() { + Some(id) => id, + None => return Some(bound), + }; + + if principal_a == trait_id { + Some(new_principal_trait_ref.clone()) + } else { + auto_trait_ids_b.contains(&trait_id).then_some(bound) + } + }), + ) + }), + lifetime: lifetime_b.clone(), + }) + .intern(interner); + + // Check that new source is equal to target + let eq_goal = EqGoal { + a: new_source_ty.cast(interner), + b: target_ty.clone().cast(interner), + } + .cast(interner); - builder.push_clause(trait_ref, [eq_goal, lifetime_outlives_goal].iter()); + // We don't push goal for `principal_b`'s object safety because it's implied by + // `principal_a`'s object safety. + builder + .push_clause(trait_ref.clone(), [eq_goal, lifetime_outlives_goal.clone()]); + } + } } // T -> dyn Trait + 'a diff --git a/tests/test/unsize.rs b/tests/test/unsize.rs index b6cdb7c03cd..795d2497450 100644 --- a/tests/test/unsize.rs +++ b/tests/test/unsize.rs @@ -179,6 +179,100 @@ fn super_auto_trait() { } } +#[test] +fn dyn_upcasting() { + test! { + program { + #[lang(unsize)] + trait Unsize {} + + #[object_safe] + trait SuperSuper {} + #[object_safe] + trait GenericSuper {} + #[object_safe] + trait Super + where + Self: SuperSuper, + Self: GenericSuper, + Self: GenericSuper, + {} + #[object_safe] + trait Principal where Self: Super {} + + #[auto] + #[object_safe] + trait Auto1 {} + + #[auto] + #[object_safe] + trait Auto2 {} + } + + goal { + forall<'a> { + dyn Principal + 'a: Unsize + } + } yields { + expect![[r#"Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"#]] + } + + goal { + forall<'a> { + dyn Principal + Auto1 + 'a: Unsize + } + } yields { + expect![[r#"Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"#]] + } + + // Different set of auto traits + goal { + forall<'a> { + dyn Principal + Auto1 + 'a: Unsize + } + } yields { + expect![[r#"No possible solution"#]] + } + + // Dropping auto traits is allowed + goal { + forall<'a> { + dyn Principal + Auto1 + Auto2 + 'a: Unsize + } + } yields { + expect![[r#"Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"#]] + } + + // Upcasting to indirect super traits + goal { + forall<'a> { + dyn Principal + 'a: Unsize + } + } yields { + expect![[r#"Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"#]] + } + + goal { + forall<'a> { + dyn Principal + 'a: Unsize + 'a> + } + } yields { + expect![[r#"Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"#]] + } + + // Ambiguous if there are multiple super traits applicable + goal { + exists { + forall<'a> { + dyn Principal + 'a: Unsize + 'a> + } + } + } yields { + expect![[r#"Ambiguous; no inference guidance"#]] + } + } +} + #[test] fn ty_to_dyn_unsizing() { test! { From 92b4a48ed2dbbd546560ba85720af7d5e954a46e Mon Sep 17 00:00:00 2001 From: Waffle Lapkin Date: Thu, 2 Jan 2025 19:15:23 +0100 Subject: [PATCH 6/7] Add a doc comment for `super_traits` Co-authored-by: Ryo Yoshida --- chalk-solve/src/clauses/super_traits.rs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/chalk-solve/src/clauses/super_traits.rs b/chalk-solve/src/clauses/super_traits.rs index eeb3678ce8d..fe2702a09d4 100644 --- a/chalk-solve/src/clauses/super_traits.rs +++ b/chalk-solve/src/clauses/super_traits.rs @@ -73,6 +73,27 @@ pub(super) fn push_trait_super_clauses( } } +/// Returns super-`TraitRef`s and super-`Projection`s that are quantified over the parameters of +/// `trait_id` and relevant higher-ranked lifetimes. The outer `Binders` is for the former and the +/// inner `Binders` is for the latter. +/// +/// For example, given the following trait definitions and `C` as `trait_id`, +/// +/// ``` +/// trait A<'a, T> {} +/// trait B<'b, U> where Self: for<'x> A<'x, U> {} +/// trait C<'c, V> where Self: B<'c, V> {} +/// ``` +/// +/// returns the following quantified `TraitRef`s. +/// +/// ```notrust +/// for { +/// for<'x> { Self: A<'x, V> } +/// for<> { Self: B<'c, V> } +/// for<> { Self: C<'c, V> } +/// } +/// ``` pub(crate) fn super_traits( db: &dyn RustIrDatabase, trait_id: TraitId, From 5689335c417e7e511a9fa37da69b3709591cfa86 Mon Sep 17 00:00:00 2001 From: Waffle Lapkin Date: Wed, 8 Jan 2025 13:37:37 +0100 Subject: [PATCH 7/7] Add a test for upcasting into a lifetimed supertrait --- tests/test/unsize.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/tests/test/unsize.rs b/tests/test/unsize.rs index 795d2497450..e3b26f52e96 100644 --- a/tests/test/unsize.rs +++ b/tests/test/unsize.rs @@ -191,11 +191,14 @@ fn dyn_upcasting() { #[object_safe] trait GenericSuper {} #[object_safe] + trait LifetimedSuper<'a> {} + #[object_safe] trait Super where Self: SuperSuper, Self: GenericSuper, Self: GenericSuper, + forall<'a> Self: LifetimedSuper<'a>, {} #[object_safe] trait Principal where Self: Super {} @@ -270,6 +273,18 @@ fn dyn_upcasting() { } yields { expect![[r#"Ambiguous; no inference guidance"#]] } + + goal { + forall<'a> { + forall<'b> { + forall<'c> { + dyn Principal + 'a: Unsize + 'c> + } + } + } + } yields { + expect!["Unique; lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!3_0 }, InEnvironment { environment: Env([]), goal: '!2_0: '!5_0 }, InEnvironment { environment: Env([]), goal: '!5_0: '!2_0 }]"] + } } }