From 91fb04d6b9000d9d932a38e20a0a3a66cbad9fa8 Mon Sep 17 00:00:00 2001 From: Yosh Date: Thu, 29 Jun 2023 02:17:26 +0200 Subject: [PATCH] update trait {decls,impls} with a `safe` prefix --- tests/associated_type_normalization.rs | 4 +- tests/coherence_orphan.rs | 50 +++++------ tests/coherence_overlap.rs | 110 ++++++++++++------------- tests/hello_world.rs | 12 +-- 4 files changed, 88 insertions(+), 88 deletions(-) diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs index 9ce3abcd..dba6ce6f 100644 --- a/tests/associated_type_normalization.rs +++ b/tests/associated_type_normalization.rs @@ -2,11 +2,11 @@ use formality::test_where_clause; const MIRROR: &str = "[ crate core { - trait Mirror<> where [] { + safe trait Mirror<> where [] { type Assoc<> : [] where []; } - impl Mirror<> for T where [] { + safe impl Mirror<> for T where [] { type Assoc<> = T where []; } } diff --git a/tests/coherence_orphan.rs b/tests/coherence_orphan.rs index 40f7df5a..0fc7c071 100644 --- a/tests/coherence_orphan.rs +++ b/tests/coherence_orphan.rs @@ -8,7 +8,7 @@ fn test_orphan_CoreTrait_for_CoreStruct_in_Foo() { expect_test::expect![[r#" Err( Error { - context: "orphan_check(impl <> CoreTrait < > for (rigid (adt CoreStruct)) where [] { })", + context: "orphan_check(safe impl <> CoreTrait < > for (rigid (adt CoreStruct)) where [] { })", source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}", }, ) @@ -16,11 +16,11 @@ fn test_orphan_CoreTrait_for_CoreStruct_in_Foo() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait<> where [] {} + safe trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} }, crate foo { - impl<> CoreTrait<> for CoreStruct<> where [] {} + safe impl<> CoreTrait<> for CoreStruct<> where [] {} } ]", )); @@ -31,7 +31,7 @@ fn test_orphan_neg_CoreTrait_for_CoreStruct_in_Foo() { expect_test::expect![[r#" Err( Error { - context: "orphan_check_neg(impl <> ! CoreTrait < > for (rigid (adt CoreStruct)) where [] {})", + context: "orphan_check_neg(safe impl <> ! CoreTrait < > for (rigid (adt CoreStruct)) where [] {})", source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}", }, ) @@ -39,11 +39,11 @@ fn test_orphan_neg_CoreTrait_for_CoreStruct_in_Foo() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait<> where [] {} + safe trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} }, crate foo { - impl<> !CoreTrait<> for CoreStruct<> where [] {} + safe impl<> !CoreTrait<> for CoreStruct<> where [] {} } ]", )); @@ -54,7 +54,7 @@ fn test_orphan_mirror_CoreStruct() { expect_test::expect![[r#" Err( Error { - context: "orphan_check(impl <> CoreTrait < > for (alias (Mirror :: Assoc) (rigid (adt CoreStruct))) where [] { })", + context: "orphan_check(safe impl <> CoreTrait < > for (alias (Mirror :: Assoc) (rigid (adt CoreStruct))) where [] { })", source: "failed to prove {@ IsLocal(CoreTrait((alias (Mirror :: Assoc) (rigid (adt CoreStruct)))))} given {}, got {}", }, ) @@ -62,19 +62,19 @@ fn test_orphan_mirror_CoreStruct() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait<> where [] {} + safe trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} - trait Mirror<> where [] { + safe trait Mirror<> where [] { type Assoc<> : [] where []; } - impl Mirror<> for T where [] { + safe impl Mirror<> for T where [] { type Assoc<> = T where []; } }, crate foo { - impl<> CoreTrait<> for as Mirror<>>::Assoc<> where [] {} + safe impl<> CoreTrait<> for as Mirror<>>::Assoc<> where [] {} } ]", )); @@ -93,19 +93,19 @@ fn test_orphan_mirror_FooStruct() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait<> where [] {} + safe trait CoreTrait<> where [] {} - trait Mirror<> where [] { + safe trait Mirror<> where [] { type Assoc<> : [] where []; } - impl Mirror<> for T where [] { + safe impl Mirror<> for T where [] { type Assoc<> = T where []; } }, crate foo { struct FooStruct<> where [] {} - impl<> CoreTrait<> for as Mirror<>>::Assoc<> where [] {} + safe impl<> CoreTrait<> for as Mirror<>>::Assoc<> where [] {} } ]", )); @@ -119,7 +119,7 @@ fn test_orphan_alias_to_unit() { expect_test::expect![[r#" Err( Error { - context: "orphan_check(impl <> CoreTrait < > for (alias (Unit :: Assoc) (rigid (adt FooStruct))) where [] { })", + context: "orphan_check(safe impl <> CoreTrait < > for (alias (Unit :: Assoc) (rigid (adt FooStruct))) where [] { })", source: "failed to prove {@ IsLocal(CoreTrait((alias (Unit :: Assoc) (rigid (adt FooStruct)))))} given {}, got {}", }, ) @@ -127,19 +127,19 @@ fn test_orphan_alias_to_unit() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait<> where [] {} + safe trait CoreTrait<> where [] {} - trait Unit<> where [] { + safe trait Unit<> where [] { type Assoc<> : [] where []; } - impl Unit<> for T where [] { + safe impl Unit<> for T where [] { type Assoc<> = () where []; } }, crate foo { struct FooStruct<> where [] {} - impl<> CoreTrait<> for as Unit<>>::Assoc<> where [] {} + safe impl<> CoreTrait<> for as Unit<>>::Assoc<> where [] {} } ]", )); @@ -150,7 +150,7 @@ fn test_orphan_uncovered_T() { expect_test::expect![[r#" Err( Error { - context: "orphan_check(impl CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { })", + context: "orphan_check(safe impl CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { })", source: "failed to prove {@ IsLocal(CoreTrait(!ty_1, (rigid (adt FooStruct))))} given {}, got {}", }, ) @@ -158,11 +158,11 @@ fn test_orphan_uncovered_T() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait where [] {} + safe trait CoreTrait where [] {} }, crate foo { struct FooStruct<> where [] {} - impl CoreTrait> for T where [] {} + safe impl CoreTrait> for T where [] {} } ]", )); @@ -178,12 +178,12 @@ fn test_orphan_covered_VecT() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait where [] {} + safe trait CoreTrait where [] {} struct Vec where [] {} }, crate foo { struct FooStruct<> where [] {} - impl CoreTrait> for Vec where [] {} + safe impl CoreTrait> for Vec where [] {} } ]", )); diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs index e3cca598..73bddc2e 100644 --- a/tests/coherence_overlap.rs +++ b/tests/coherence_overlap.rs @@ -14,9 +14,9 @@ fn test_u32_i32_impls() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait Foo<> where [] {} - impl<> Foo<> for u32 where [] {} - impl<> Foo<> for i32 where [] {} + safe trait Foo<> where [] {} + safe impl<> Foo<> for u32 where [] {} + safe impl<> Foo<> for i32 where [] {} } ]", )); @@ -27,15 +27,15 @@ fn test_u32_u32_impls() { // Test that we detect duplicate impls. expect_test::expect![[r#" Err( - "duplicate impl in current crate: impl <> Foo < > for (rigid (scalar u32)) where [] { }", + "duplicate impl in current crate: safe impl <> Foo < > for (rigid (scalar u32)) where [] { }", ) "#]] .assert_debug_eq(&test_program_ok( "[ crate core { - trait Foo<> where [] {} - impl<> Foo<> for u32 where [] {} - impl<> Foo<> for u32 where [] {} + safe trait Foo<> where [] {} + safe impl<> Foo<> for u32 where [] {} + safe impl<> Foo<> for u32 where [] {} } ]", )); @@ -46,15 +46,15 @@ fn test_u32_T_impls() { // Test that we detect overlap involving generic parameters. expect_test::expect![[r#" Err( - "impls may overlap: `impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `impl Foo < > for ^ty0_0 where [] { }`", + "impls may overlap: `safe impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `safe impl Foo < > for ^ty0_0 where [] { }`", ) "#]] .assert_debug_eq(&test_program_ok( "[ crate core { - trait Foo<> where [] {} - impl<> Foo<> for u32 where [] {} - impl Foo<> for T where [] {} + safe trait Foo<> where [] {} + safe impl<> Foo<> for u32 where [] {} + safe impl Foo<> for T where [] {} } ]", )); @@ -74,11 +74,11 @@ fn test_u32_T_where_T_Not_impls() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait Foo<> where [] {} - impl<> Foo<> for u32 where [] {} - impl Foo<> for T where [T: Not<>] {} + safe trait Foo<> where [] {} + safe impl<> Foo<> for u32 where [] {} + safe impl Foo<> for T where [T: Not<>] {} - trait Not<> where [] {} + safe trait Not<> where [] {} } ]", )); @@ -90,18 +90,18 @@ fn test_u32_T_where_T_Is_impls() { // and also all `T: Is`, and `u32: Is`. expect_test::expect![[r#" Err( - "impls may overlap: `impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `impl Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`", + "impls may overlap: `safe impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `safe impl Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`", ) "#]] .assert_debug_eq(&test_program_ok( "[ crate core { - trait Foo<> where [] {} - impl<> Foo<> for u32 where [] {} - impl Foo<> for T where [T: Is<>] {} + safe trait Foo<> where [] {} + safe impl<> Foo<> for u32 where [] {} + safe impl Foo<> for T where [T: Is<>] {} - trait Is<> where [] {} - impl<> Is<> for u32 where [] {} + safe trait Is<> where [] {} + safe impl<> Is<> for u32 where [] {} } ]", )); @@ -113,7 +113,7 @@ fn test_u32_not_u32_impls() { expect_test::expect![[r#" Err( Error { - context: "check_trait_impl(impl <> Foo < > for (rigid (scalar u32)) where [] { })", + context: "check_trait_impl(safe impl <> Foo < > for (rigid (scalar u32)) where [] { })", source: "failed to disprove {! Foo((rigid (scalar u32)))} given {}, got {Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }}", }, ) @@ -121,9 +121,9 @@ fn test_u32_not_u32_impls() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait Foo<> where [] {} - impl<> Foo<> for u32 where [] {} - impl<> !Foo<> for u32 where [] {} + safe trait Foo<> where [] {} + safe impl<> Foo<> for u32 where [] {} + safe impl<> !Foo<> for u32 where [] {} } ]", )); @@ -139,7 +139,7 @@ fn test_T_where_Foo_not_u32_impls() { expect_test::expect![[r#" Err( Error { - context: "check_trait_impl(impl Foo < > for ^ty0_0 where [^ty0_0 : Foo < >] { })", + context: "check_trait_impl(safe impl Foo < > for ^ty0_0 where [^ty0_0 : Foo < >] { })", source: "failed to disprove {! Foo(!ty_1)} given {Foo(!ty_1)}, got {Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => (rigid (scalar u32))} }}", }, ) @@ -147,9 +147,9 @@ fn test_T_where_Foo_not_u32_impls() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait Foo<> where [] {} - impl Foo<> for T where [T: Foo<>] {} - impl<> !Foo<> for u32 where [] {} + safe trait Foo<> where [] {} + safe impl Foo<> for T where [T: Foo<>] {} + safe impl<> !Foo<> for u32 where [] {} } ]", )); @@ -159,19 +159,19 @@ fn test_T_where_Foo_not_u32_impls() { fn test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait() { expect_test::expect![[r#" Err( - "impls may overlap: `impl FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs `impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`", + "impls may overlap: `safe impl FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs `safe impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`", ) "#]] .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait<> where [] {} + safe trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} }, crate foo { - trait FooTrait<> where [] {} - impl FooTrait<> for T where [T: CoreTrait<>] {} - impl<> FooTrait<> for CoreStruct<> where [] {} + safe trait FooTrait<> where [] {} + safe impl FooTrait<> for T where [T: CoreTrait<>] {} + safe impl<> FooTrait<> for CoreStruct<> where [] {} } ]", )); @@ -190,14 +190,14 @@ fn test_neg_CoreTrait_for_CoreStruct_implies_no_overlap() { .assert_debug_eq(&test_program_ok( "[ crate core { - trait CoreTrait<> where [] {} + safe trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} - impl<> !CoreTrait<> for CoreStruct<> where [] {} + safe impl<> !CoreTrait<> for CoreStruct<> where [] {} }, crate foo { - trait FooTrait<> where [] {} - impl FooTrait<> for T where [T: CoreTrait<>] {} - impl<> FooTrait<> for CoreStruct<> where [] {} + safe trait FooTrait<> where [] {} + safe impl FooTrait<> for T where [T: CoreTrait<>] {} + safe impl<> FooTrait<> for CoreStruct<> where [] {} } ]", )); @@ -211,24 +211,24 @@ fn test_overlap_normalize_alias_to_LocalType() { let gen_program = |addl: &str| { const BASE_PROGRAM: &str = "[ crate core { - trait Iterator<> where [] { + safe trait Iterator<> where [] { } - trait Mirror<> where [] { + safe trait Mirror<> where [] { type T<> : [] where []; } - impl Mirror<> for A where [] { + safe impl Mirror<> for A where [] { type T<> = A where []; } struct LocalType<> where [] {} - trait LocalTrait<> where [] { } + safe trait LocalTrait<> where [] { } - impl LocalTrait<> for T where [T: Iterator<>] { } + safe impl LocalTrait<> for T where [T: Iterator<>] { } - impl<> LocalTrait<> for ::T where [] { } + safe impl<> LocalTrait<> for ::T where [] { } ADDITIONAL } @@ -253,10 +253,10 @@ fn test_overlap_normalize_alias_to_LocalType() { expect_test::expect![[r#" Err( - "impls may overlap: `impl LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs `impl <> LocalTrait < > for (alias (Mirror :: T) (rigid (adt LocalType))) where [] { }`", + "impls may overlap: `safe impl LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs `safe impl <> LocalTrait < > for (alias (Mirror :: T) (rigid (adt LocalType))) where [] { }`", ) "#]] - .assert_debug_eq(&test_program_ok(&gen_program("impl<> Iterator<> for LocalType<> where [] {}"))); + .assert_debug_eq(&test_program_ok(&gen_program("safe impl<> Iterator<> for LocalType<> where [] {}"))); } #[test] @@ -267,24 +267,24 @@ fn test_overlap_alias_not_normalizable() { let gen_program = |addl: &str| { const BASE_PROGRAM: &str = "[ crate core { - trait Iterator<> where [] { + safe trait Iterator<> where [] { } - trait Mirror<> where [] { + safe trait Mirror<> where [] { type T<> : [] where []; } - impl Mirror<> for A where [] { + safe impl Mirror<> for A where [] { type T<> = A where []; } struct LocalType<> where [] {} - trait LocalTrait<> where [] { } + safe trait LocalTrait<> where [] { } - impl LocalTrait<> for T where [T: Iterator<>] { } + safe impl LocalTrait<> for T where [T: Iterator<>] { } - impl LocalTrait<> for ::T where [T: Mirror<>] { } + safe impl LocalTrait<> for ::T where [T: Mirror<>] { } ADDITIONAL } @@ -312,10 +312,10 @@ fn test_overlap_alias_not_normalizable() { expect_test::expect![[r#" Err( - "impls may overlap: `impl LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs `impl LocalTrait < > for (alias (Mirror :: T) ^ty0_0) where [^ty0_0 : Mirror < >] { }`", + "impls may overlap: `safe impl LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs `safe impl LocalTrait < > for (alias (Mirror :: T) ^ty0_0) where [^ty0_0 : Mirror < >] { }`", ) "#]] // FIXME .assert_debug_eq(&test_program_ok(&gen_program( - "impl<> Iterator<> for u32 where[] {}", + "safe impl<> Iterator<> for u32 where[] {}", ))); } diff --git a/tests/hello_world.rs b/tests/hello_world.rs index 1865d578..e2cd7ca5 100644 --- a/tests/hello_world.rs +++ b/tests/hello_world.rs @@ -12,11 +12,11 @@ fn test_broken() { "#]].assert_debug_eq(&test_program_ok( "[ crate Foo { - trait Foo where [T: Bar] {} + safe trait Foo where [T: Bar] {} - trait Bar where [T: Baz<>] {} + safe trait Bar where [T: Baz<>] {} - trait Baz<> where [] {} + safe trait Baz<> where [] {} } ]", )); @@ -32,11 +32,11 @@ fn test_ok() { .assert_debug_eq(&test_program_ok( "[ crate Foo { - trait Foo where [T: Bar, Self: Baz<>] {} + safe trait Foo where [T: Bar, Self: Baz<>] {} - trait Bar where [T: Baz<>] {} + safe trait Bar where [T: Baz<>] {} - trait Baz<> where [] {} + safe trait Baz<> where [] {} } ]", ));