From 0c78cd6823ece8e3cf0b65a71526ad8f9b1621d3 Mon Sep 17 00:00:00 2001 From: Yosh Date: Thu, 29 Jun 2023 00:50:57 +0200 Subject: [PATCH 1/6] add failing unsafe traits test --- tests/unsafe-trait.rs | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tests/unsafe-trait.rs diff --git a/tests/unsafe-trait.rs b/tests/unsafe-trait.rs new file mode 100644 index 00000000..7199f585 --- /dev/null +++ b/tests/unsafe-trait.rs @@ -0,0 +1,37 @@ +use formality::test_program_ok; + +#[test] +fn unsafe_trait_requires_unsafe_impl_err() { + expect_test::expect![[r#" + Err( + (), + ) + "#]] + .assert_debug_eq(&test_program_ok( + "[ + crate core { + unsafe trait SendTrait<> where [] {} + struct SendStruct<> where [] {} + impl<> SendTrait for SendStruct where [] {} + } + ]", + )); +} + +#[test] +fn unsafe_trait_requires_unsafe_impl() { + expect_test::expect![[r#" + Ok( + (), + ) + "#]] + .assert_debug_eq(&test_program_ok( + "[ + crate core { + unsafe trait SendTrait<> where [] {} + struct SendStruct<> where [] {} + unsafe impl<> SendTrait for SendStruct where [] {} + } + ]", + )); +} From 7e83206bb3e23258095ef7152bd5744410d63abd Mon Sep 17 00:00:00 2001 From: Yosh Date: Thu, 29 Jun 2023 02:16:55 +0200 Subject: [PATCH 2/6] implement `unsafe trait` support --- crates/formality-check/src/impls.rs | 21 +++++++++++++++++++-- crates/formality-check/src/traits.rs | 6 +++++- crates/formality-prove/src/decls.rs | 15 ++++++++++++--- crates/formality-rust/src/grammar.rs | 10 +++++++--- crates/formality-rust/src/prove.rs | 12 ++++++++---- tests/unsafe-trait.rs | 13 ++++++++----- 6 files changed, 59 insertions(+), 18 deletions(-) diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 1fb4ae7d..fe18f224 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -1,7 +1,7 @@ use anyhow::bail; use fn_error_context::context; -use formality_prove::Env; +use formality_prove::{Env, Safety}; use formality_rust::{ grammar::{ AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Fn, @@ -19,7 +19,7 @@ use formality_types::{ impl super::Check<'_> { #[context("check_trait_impl({v:?})")] pub(super) fn check_trait_impl(&self, v: &TraitImpl) -> Fallible<()> { - let TraitImpl { binder } = v; + let TraitImpl { binder, safety } = v; let mut env = Env::default(); @@ -45,6 +45,8 @@ impl super::Check<'_> { trait_items, } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?; + self.check_safety_matches(&trait_decl.safety, safety)?; + for impl_item in &impl_items { self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?; } @@ -71,6 +73,21 @@ impl super::Check<'_> { Ok(()) } + /// Validate `unsafe trait` and `unsafe impl` line up + fn check_safety_matches(&self, trait_decl: &Safety, trait_impl: &Safety) -> Fallible<()> { + match trait_decl { + Safety::Safe => anyhow::ensure!( + matches!(trait_impl, Safety::Safe), + "implementing the trait is not `unsafe`" + ), + Safety::Unsafe => anyhow::ensure!( + matches!(trait_impl, Safety::Unsafe), + "the trait requires an `unsafe impl` declaration" + ), + } + Ok(()) + } + fn check_trait_impl_item( &self, env: &Env, diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs index 1347ce92..22791031 100644 --- a/crates/formality-check/src/traits.rs +++ b/crates/formality-check/src/traits.rs @@ -8,7 +8,11 @@ use formality_types::grammar::Fallible; impl super::Check<'_> { #[context("check_trait({:?})", t.id)] pub(super) fn check_trait(&self, t: &Trait) -> Fallible<()> { - let Trait { id: _, binder } = t; + let Trait { + safety: _, + id: _, + binder, + } = t; let mut env = Env::default(); let TraitBoundData { diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 4b7b170c..69949fc2 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -95,8 +95,9 @@ impl Decls { } } -#[term(impl $binder)] +#[term($safety impl $binder)] pub struct ImplDecl { + pub safety: Safety, pub binder: Binder, } @@ -106,8 +107,9 @@ pub struct ImplDeclBoundData { pub where_clause: Wcs, } -#[term(impl $binder)] +#[term($safety impl $binder)] pub struct NegImplDecl { + pub safety: Safety, pub binder: Binder, } @@ -117,8 +119,15 @@ pub struct NegImplDeclBoundData { pub where_clause: Wcs, } -#[term(trait $id $binder)] +#[term] +pub enum Safety { + Safe, + Unsafe, +} + +#[term($safety trait $id $binder)] pub struct TraitDecl { + pub safety: Safety, pub id: TraitId, pub binder: Binder, } diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index a77d8ab9..6cb2cb0c 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -1,6 +1,7 @@ use std::sync::Arc; use formality_macros::term; +use formality_prove::Safety; use formality_types::{ cast::Upcast, grammar::{ @@ -161,8 +162,9 @@ pub struct Variant { pub fields: Vec, } -#[term(trait $id $binder)] +#[term($safety trait $id $binder)] pub struct Trait { + pub safety: Safety, pub id: TraitId, pub binder: TraitBinder, } @@ -242,8 +244,9 @@ pub struct AssociatedTyBoundData { pub where_clauses: Vec, } -#[term(impl $binder)] +#[term($safety impl $binder)] pub struct TraitImpl { + pub safety: Safety, pub binder: Binder, } @@ -268,8 +271,9 @@ impl TraitImplBoundData { } } -#[term(impl $binder)] +#[term($safety impl $binder)] pub struct NegTraitImpl { + pub safety: Safety, pub binder: Binder, } diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 7264326f..ff2ddf8e 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -80,7 +80,7 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::Trait(Trait { id, binder }) => { + CrateItem::Trait(Trait { id, binder, safety }) => { let ( vars, TraitBoundData { @@ -89,6 +89,7 @@ impl Crate { }, ) = binder.open(); Some(prove::TraitDecl { + safety: safety.clone(), id: id.clone(), binder: Binder::new( &vars, @@ -110,7 +111,7 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::TraitImpl(TraitImpl { binder }) => { + CrateItem::TraitImpl(TraitImpl { binder, safety }) => { let ( vars, TraitImplBoundData { @@ -122,6 +123,7 @@ impl Crate { }, ) = binder.open(); Some(prove::ImplDecl { + safety: safety.clone(), binder: Binder::new( &vars, prove::ImplDeclBoundData { @@ -140,7 +142,7 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::NegTraitImpl(NegTraitImpl { binder }) => { + CrateItem::NegTraitImpl(NegTraitImpl { binder, safety }) => { let ( vars, NegTraitImplBoundData { @@ -151,6 +153,7 @@ impl Crate { }, ) = binder.open(); Some(prove::NegImplDecl { + safety: safety.clone(), binder: Binder::new( &vars, prove::NegImplDeclBoundData { @@ -169,7 +172,7 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::TraitImpl(TraitImpl { binder }) => { + CrateItem::TraitImpl(TraitImpl { binder, safety: _ }) => { let ( impl_vars, TraitImplBoundData { @@ -225,6 +228,7 @@ impl Crate { .iter() .flat_map(|item| match item { CrateItem::Trait(Trait { + safety: _, id: trait_id, binder, }) => { diff --git a/tests/unsafe-trait.rs b/tests/unsafe-trait.rs index 7199f585..2b6626fb 100644 --- a/tests/unsafe-trait.rs +++ b/tests/unsafe-trait.rs @@ -4,7 +4,10 @@ use formality::test_program_ok; fn unsafe_trait_requires_unsafe_impl_err() { expect_test::expect![[r#" Err( - (), + Error { + context: "check_trait_impl(safe impl <> SendTrait < > for (rigid (adt SendStruct)) where [] { })", + source: "the trait requires an `unsafe impl` declaration", + }, ) "#]] .assert_debug_eq(&test_program_ok( @@ -12,7 +15,7 @@ fn unsafe_trait_requires_unsafe_impl_err() { crate core { unsafe trait SendTrait<> where [] {} struct SendStruct<> where [] {} - impl<> SendTrait for SendStruct where [] {} + safe impl<> SendTrait<> for SendStruct<> where [] {} } ]", )); @@ -28,9 +31,9 @@ fn unsafe_trait_requires_unsafe_impl() { .assert_debug_eq(&test_program_ok( "[ crate core { - unsafe trait SendTrait<> where [] {} - struct SendStruct<> where [] {} - unsafe impl<> SendTrait for SendStruct where [] {} + unsafe trait CoreTrait<> where [] {} + struct CoreStruct<> where [] {} + unsafe impl<> CoreTrait<> for CoreStruct<> where [] {} } ]", )); From 89368428443ac216f6ef028a64754df6b76f2ba9 Mon Sep 17 00:00:00 2001 From: Yosh Date: Thu, 29 Jun 2023 02:17:26 +0200 Subject: [PATCH 3/6] update trait {decls,impls} with a `safe` prefix --- .../formality-prove/src/test/eq_partial_eq.rs | 4 +- .../src/test/exists_constraints.rs | 4 +- crates/formality-prove/src/test/expanding.rs | 4 +- crates/formality-prove/src/test/magic_copy.rs | 8 +- .../formality-prove/src/test/occurs_check.rs | 4 +- .../formality-prove/src/test/simple_impl.rs | 6 +- crates/formality-prove/src/test/universes.rs | 4 +- tests/associated_type_normalization.rs | 4 +- tests/coherence_orphan.rs | 50 ++++---- tests/coherence_overlap.rs | 110 +++++++++--------- tests/hello_world.rs | 12 +- 11 files changed, 105 insertions(+), 105 deletions(-) diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index bdfff075..f1868f2e 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -11,8 +11,8 @@ use crate::{decls::Decls, prove::prove}; fn decls() -> Decls { Decls { trait_decls: vec![ - term("trait Eq where {PartialEq(Self)}"), - term("trait PartialEq where {}"), + term("safe trait Eq where {PartialEq(Self)}"), + term("safe trait PartialEq where {}"), ], ..Decls::empty() } diff --git a/crates/formality-prove/src/test/exists_constraints.rs b/crates/formality-prove/src/test/exists_constraints.rs index 9b5ba9ac..b912d6f1 100644 --- a/crates/formality-prove/src/test/exists_constraints.rs +++ b/crates/formality-prove/src/test/exists_constraints.rs @@ -9,8 +9,8 @@ use crate::test_util::test_prove; /// Simple example decls consisting only of two trait declarations. fn decls() -> Decls { Decls { - trait_decls: vec![term("trait Foo where {}")], - impl_decls: vec![term("impl Foo(Vec) where {}")], + trait_decls: vec![term("safe trait Foo where {}")], + impl_decls: vec![term("safe impl Foo(Vec) where {}")], ..Decls::empty() } } diff --git a/crates/formality-prove/src/test/expanding.rs b/crates/formality-prove/src/test/expanding.rs index 06c931c0..9aa4d67d 100644 --- a/crates/formality-prove/src/test/expanding.rs +++ b/crates/formality-prove/src/test/expanding.rs @@ -8,8 +8,8 @@ use crate::{test_util::test_prove, Decls}; fn decls() -> Decls { Decls { max_size: 10, - trait_decls: vec![term("trait Debug where {}")], - impl_decls: vec![term("impl Debug(Vec) where {Debug(T)}")], + trait_decls: vec![term("safe trait Debug where {}")], + impl_decls: vec![term("safe impl Debug(Vec) where {Debug(T)}")], ..Decls::empty() } } diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index a3327cbb..549f64f5 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -10,12 +10,12 @@ use crate::test_util::test_prove; fn decls() -> Decls { Decls { trait_decls: vec![ - term("trait Copy where {}"), - term("trait Magic where {Copy(Self)}"), + term("safe trait Copy where {}"), + term("safe trait Magic where {Copy(Self)}"), ], impl_decls: vec![ - term("impl Magic(T) where {Magic(T)}"), - term("impl<> Copy(u32) where {}"), + term("safe impl Magic(T) where {Magic(T)}"), + term("safe impl<> Copy(u32) where {}"), ], ..Decls::empty() } diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs index 8bd3dcae..5acc3fa2 100644 --- a/crates/formality-prove/src/test/occurs_check.rs +++ b/crates/formality-prove/src/test/occurs_check.rs @@ -9,8 +9,8 @@ use crate::test_util::test_prove; /// Simple example decls consisting only of two trait declarations. fn decls() -> Decls { Decls { - trait_decls: vec![term("trait Foo where {}")], - impl_decls: vec![term("impl Foo(Vec) where {}")], + trait_decls: vec![term("safe trait Foo where {}")], + impl_decls: vec![term("safe impl Foo(Vec) where {}")], ..Decls::empty() } } diff --git a/crates/formality-prove/src/test/simple_impl.rs b/crates/formality-prove/src/test/simple_impl.rs index 591c7347..83b1139d 100644 --- a/crates/formality-prove/src/test/simple_impl.rs +++ b/crates/formality-prove/src/test/simple_impl.rs @@ -7,10 +7,10 @@ use crate::{decls::Decls, prove::prove}; /// Simple example decls consisting only of two trait declarations. fn decls() -> Decls { Decls { - trait_decls: vec![term("trait Debug where {}")], + trait_decls: vec![term("safe trait Debug where {}")], impl_decls: vec![ - term("impl Debug(Vec) where {Debug(T)}"), - term("impl<> Debug(u32) where {}"), + term("safe impl Debug(Vec) where {Debug(T)}"), + term("safe impl<> Debug(u32) where {}"), ], ..Decls::empty() } diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs index de0f9ab9..b578f700 100644 --- a/crates/formality-prove/src/test/universes.rs +++ b/crates/formality-prove/src/test/universes.rs @@ -21,8 +21,8 @@ fn exists_u_for_t() { #[test] fn for_t_exists_u() { let decls = Decls { - trait_decls: vec![term("trait Test where {}")], - impl_decls: vec![term("impl Test(X, Y) where {X = Y}")], + trait_decls: vec![term("safe trait Test where {}")], + impl_decls: vec![term("safe impl Test(X, Y) where {X = Y}")], ..Decls::empty() }; 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 [] {} } ]", )); From 77673954d099436ec6d9e54c81dd8f4ef34824c3 Mon Sep 17 00:00:00 2001 From: Yosh Date: Thu, 29 Jun 2023 11:44:24 +0200 Subject: [PATCH 4/6] hand-roll parser for `enum Safety` --- crates/formality-prove/src/decls.rs | 52 ++++++++++++++++++++++++++++- crates/formality-types/src/parse.rs | 9 +++++ 2 files changed, 60 insertions(+), 1 deletion(-) diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 69949fc2..78ebb817 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -2,11 +2,16 @@ use formality_macros::term; use formality_types::{ cast::Upcast, collections::Set, + derive_links::{DowncastTo, UpcastFrom}, + fold::Fold, grammar::{ AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs, PR, }, + parse::{self, Parse}, set, + term::Term, + visit::Visit, }; #[term] @@ -119,12 +124,57 @@ pub struct NegImplDeclBoundData { pub where_clause: Wcs, } -#[term] +/// Mark a trait or trait impl as `unsafe`. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum Safety { Safe, Unsafe, } +impl Term for Safety {} + +impl DowncastTo for Safety { + fn downcast_to(&self) -> Option { + Some(Self::clone(self)) + } +} + +impl UpcastFrom for Safety { + fn upcast_from(term: Self) -> Self { + term + } +} + +impl Fold for Safety { + fn substitute(&self, _substitution_fn: formality_types::fold::SubstitutionFn<'_>) -> Self { + self.clone() + } +} + +impl Visit for Safety { + fn free_variables(&self) -> Vec { + vec![] + } + + fn size(&self) -> usize { + 1 + } + + fn assert_valid(&self) {} +} + +impl Parse for Safety { + fn parse<'t>( + _scope: &formality_types::parse::Scope, + text0: &'t str, + ) -> formality_types::parse::ParseResult<'t, Self> { + match parse::expect_optional_keyword("unsafe", text0) { + Some(text1) => Ok((Self::Unsafe, text1)), + None => Ok((Self::Safe, text0)), + } + } +} + #[term($safety trait $id $binder)] pub struct TraitDecl { pub safety: Safety, diff --git a/crates/formality-types/src/parse.rs b/crates/formality-types/src/parse.rs index ce0c58ac..ab43587e 100644 --- a/crates/formality-types/src/parse.rs +++ b/crates/formality-types/src/parse.rs @@ -347,6 +347,15 @@ pub fn expect_keyword<'t>(expected: &str, text0: &'t str) -> ParseResult<'t, ()> } } +/// Attempt to consume next identifier if it is equal to `expected`. +#[tracing::instrument(level = "trace", ret)] +pub fn expect_optional_keyword<'t>(expected: &str, text0: &'t str) -> Option<&'t str> { + match identifier(text0) { + Ok((ident, text1)) if &*ident == expected => Some(text1), + _ => None, + } +} + /// Reject next identifier if it is the given keyword. Consumes nothing. #[tracing::instrument(level = "trace", ret)] pub fn reject_keyword<'t>(expected: &str, text0: &'t str) -> ParseResult<'t, ()> { From 4a6523ff1e89d5b5c67ccfea3b9aa045f29009c5 Mon Sep 17 00:00:00 2001 From: Yosh Date: Thu, 29 Jun 2023 11:57:09 +0200 Subject: [PATCH 5/6] remove the `safe trait` notation --- .../formality-prove/src/test/eq_partial_eq.rs | 4 +- .../src/test/exists_constraints.rs | 4 +- crates/formality-prove/src/test/expanding.rs | 4 +- crates/formality-prove/src/test/magic_copy.rs | 8 +- .../formality-prove/src/test/occurs_check.rs | 4 +- .../formality-prove/src/test/simple_impl.rs | 6 +- crates/formality-prove/src/test/universes.rs | 4 +- tests/associated_type_normalization.rs | 4 +- tests/coherence_orphan.rs | 50 ++++---- tests/coherence_overlap.rs | 110 +++++++++--------- tests/hello_world.rs | 12 +- tests/unsafe-trait.rs | 4 +- 12 files changed, 107 insertions(+), 107 deletions(-) diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index f1868f2e..bdfff075 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -11,8 +11,8 @@ use crate::{decls::Decls, prove::prove}; fn decls() -> Decls { Decls { trait_decls: vec![ - term("safe trait Eq where {PartialEq(Self)}"), - term("safe trait PartialEq where {}"), + term("trait Eq where {PartialEq(Self)}"), + term("trait PartialEq where {}"), ], ..Decls::empty() } diff --git a/crates/formality-prove/src/test/exists_constraints.rs b/crates/formality-prove/src/test/exists_constraints.rs index b912d6f1..9b5ba9ac 100644 --- a/crates/formality-prove/src/test/exists_constraints.rs +++ b/crates/formality-prove/src/test/exists_constraints.rs @@ -9,8 +9,8 @@ use crate::test_util::test_prove; /// Simple example decls consisting only of two trait declarations. fn decls() -> Decls { Decls { - trait_decls: vec![term("safe trait Foo where {}")], - impl_decls: vec![term("safe impl Foo(Vec) where {}")], + trait_decls: vec![term("trait Foo where {}")], + impl_decls: vec![term("impl Foo(Vec) where {}")], ..Decls::empty() } } diff --git a/crates/formality-prove/src/test/expanding.rs b/crates/formality-prove/src/test/expanding.rs index 9aa4d67d..06c931c0 100644 --- a/crates/formality-prove/src/test/expanding.rs +++ b/crates/formality-prove/src/test/expanding.rs @@ -8,8 +8,8 @@ use crate::{test_util::test_prove, Decls}; fn decls() -> Decls { Decls { max_size: 10, - trait_decls: vec![term("safe trait Debug where {}")], - impl_decls: vec![term("safe impl Debug(Vec) where {Debug(T)}")], + trait_decls: vec![term("trait Debug where {}")], + impl_decls: vec![term("impl Debug(Vec) where {Debug(T)}")], ..Decls::empty() } } diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index 549f64f5..a3327cbb 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -10,12 +10,12 @@ use crate::test_util::test_prove; fn decls() -> Decls { Decls { trait_decls: vec![ - term("safe trait Copy where {}"), - term("safe trait Magic where {Copy(Self)}"), + term("trait Copy where {}"), + term("trait Magic where {Copy(Self)}"), ], impl_decls: vec![ - term("safe impl Magic(T) where {Magic(T)}"), - term("safe impl<> Copy(u32) where {}"), + term("impl Magic(T) where {Magic(T)}"), + term("impl<> Copy(u32) where {}"), ], ..Decls::empty() } diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs index 5acc3fa2..8bd3dcae 100644 --- a/crates/formality-prove/src/test/occurs_check.rs +++ b/crates/formality-prove/src/test/occurs_check.rs @@ -9,8 +9,8 @@ use crate::test_util::test_prove; /// Simple example decls consisting only of two trait declarations. fn decls() -> Decls { Decls { - trait_decls: vec![term("safe trait Foo where {}")], - impl_decls: vec![term("safe impl Foo(Vec) where {}")], + trait_decls: vec![term("trait Foo where {}")], + impl_decls: vec![term("impl Foo(Vec) where {}")], ..Decls::empty() } } diff --git a/crates/formality-prove/src/test/simple_impl.rs b/crates/formality-prove/src/test/simple_impl.rs index 83b1139d..591c7347 100644 --- a/crates/formality-prove/src/test/simple_impl.rs +++ b/crates/formality-prove/src/test/simple_impl.rs @@ -7,10 +7,10 @@ use crate::{decls::Decls, prove::prove}; /// Simple example decls consisting only of two trait declarations. fn decls() -> Decls { Decls { - trait_decls: vec![term("safe trait Debug where {}")], + trait_decls: vec![term("trait Debug where {}")], impl_decls: vec![ - term("safe impl Debug(Vec) where {Debug(T)}"), - term("safe impl<> Debug(u32) where {}"), + term("impl Debug(Vec) where {Debug(T)}"), + term("impl<> Debug(u32) where {}"), ], ..Decls::empty() } diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs index b578f700..de0f9ab9 100644 --- a/crates/formality-prove/src/test/universes.rs +++ b/crates/formality-prove/src/test/universes.rs @@ -21,8 +21,8 @@ fn exists_u_for_t() { #[test] fn for_t_exists_u() { let decls = Decls { - trait_decls: vec![term("safe trait Test where {}")], - impl_decls: vec![term("safe impl Test(X, Y) where {X = Y}")], + trait_decls: vec![term("trait Test where {}")], + impl_decls: vec![term("impl Test(X, Y) where {X = Y}")], ..Decls::empty() }; diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs index dba6ce6f..9ce3abcd 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 { - safe trait Mirror<> where [] { + trait Mirror<> where [] { type Assoc<> : [] where []; } - safe impl Mirror<> for T where [] { + impl Mirror<> for T where [] { type Assoc<> = T where []; } } diff --git a/tests/coherence_orphan.rs b/tests/coherence_orphan.rs index 0fc7c071..c7d78c77 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(safe 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 { - safe trait CoreTrait<> where [] {} + trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} }, crate foo { - safe impl<> CoreTrait<> for CoreStruct<> where [] {} + 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(safe 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 { - safe trait CoreTrait<> where [] {} + trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} }, crate foo { - safe impl<> !CoreTrait<> for CoreStruct<> where [] {} + impl<> !CoreTrait<> for CoreStruct<> where [] {} } ]", )); @@ -54,7 +54,7 @@ fn test_orphan_mirror_CoreStruct() { expect_test::expect![[r#" Err( Error { - context: "orphan_check(safe 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 { - safe trait CoreTrait<> where [] {} + trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} - safe trait Mirror<> where [] { + trait Mirror<> where [] { type Assoc<> : [] where []; } - safe impl Mirror<> for T where [] { + impl Mirror<> for T where [] { type Assoc<> = T where []; } }, crate foo { - safe impl<> CoreTrait<> for as Mirror<>>::Assoc<> where [] {} + impl<> CoreTrait<> for as Mirror<>>::Assoc<> where [] {} } ]", )); @@ -93,19 +93,19 @@ fn test_orphan_mirror_FooStruct() { .assert_debug_eq(&test_program_ok( "[ crate core { - safe trait CoreTrait<> where [] {} + trait CoreTrait<> where [] {} - safe trait Mirror<> where [] { + trait Mirror<> where [] { type Assoc<> : [] where []; } - safe impl Mirror<> for T where [] { + impl Mirror<> for T where [] { type Assoc<> = T where []; } }, crate foo { struct FooStruct<> where [] {} - safe impl<> CoreTrait<> for as Mirror<>>::Assoc<> where [] {} + 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(safe 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 { - safe trait CoreTrait<> where [] {} + trait CoreTrait<> where [] {} - safe trait Unit<> where [] { + trait Unit<> where [] { type Assoc<> : [] where []; } - safe impl Unit<> for T where [] { + impl Unit<> for T where [] { type Assoc<> = () where []; } }, crate foo { struct FooStruct<> where [] {} - safe impl<> CoreTrait<> for as Unit<>>::Assoc<> where [] {} + 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(safe 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 { - safe trait CoreTrait where [] {} + trait CoreTrait where [] {} }, crate foo { struct FooStruct<> where [] {} - safe impl CoreTrait> for T where [] {} + impl CoreTrait> for T where [] {} } ]", )); @@ -178,12 +178,12 @@ fn test_orphan_covered_VecT() { .assert_debug_eq(&test_program_ok( "[ crate core { - safe trait CoreTrait where [] {} + trait CoreTrait where [] {} struct Vec where [] {} }, crate foo { struct FooStruct<> where [] {} - safe impl CoreTrait> for Vec where [] {} + impl CoreTrait> for Vec where [] {} } ]", )); diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs index 73bddc2e..98a50f1e 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 { - safe trait Foo<> where [] {} - safe impl<> Foo<> for u32 where [] {} - safe impl<> Foo<> for i32 where [] {} + trait Foo<> where [] {} + impl<> Foo<> for u32 where [] {} + 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: safe 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 { - safe trait Foo<> where [] {} - safe impl<> Foo<> for u32 where [] {} - safe impl<> Foo<> for u32 where [] {} + trait Foo<> where [] {} + impl<> Foo<> for u32 where [] {} + 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: `safe impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `safe 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 { - safe trait Foo<> where [] {} - safe impl<> Foo<> for u32 where [] {} - safe impl Foo<> for T where [] {} + trait Foo<> where [] {} + impl<> Foo<> for u32 where [] {} + 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 { - safe trait Foo<> where [] {} - safe impl<> Foo<> for u32 where [] {} - safe impl Foo<> for T where [T: Not<>] {} + trait Foo<> where [] {} + impl<> Foo<> for u32 where [] {} + impl Foo<> for T where [T: Not<>] {} - safe trait Not<> where [] {} + 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: `safe impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `safe 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 { - safe trait Foo<> where [] {} - safe impl<> Foo<> for u32 where [] {} - safe impl Foo<> for T where [T: Is<>] {} + trait Foo<> where [] {} + impl<> Foo<> for u32 where [] {} + impl Foo<> for T where [T: Is<>] {} - safe trait Is<> where [] {} - safe impl<> Is<> for u32 where [] {} + trait Is<> where [] {} + 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(safe 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 { - safe trait Foo<> where [] {} - safe impl<> Foo<> for u32 where [] {} - safe impl<> !Foo<> for u32 where [] {} + trait Foo<> where [] {} + impl<> Foo<> for u32 where [] {} + 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(safe 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 { - safe trait Foo<> where [] {} - safe impl Foo<> for T where [T: Foo<>] {} - safe impl<> !Foo<> for u32 where [] {} + trait Foo<> where [] {} + impl Foo<> for T where [T: Foo<>] {} + 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: `safe impl FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs `safe 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 { - safe trait CoreTrait<> where [] {} + trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} }, crate foo { - safe trait FooTrait<> where [] {} - safe impl FooTrait<> for T where [T: CoreTrait<>] {} - safe impl<> FooTrait<> for CoreStruct<> where [] {} + trait FooTrait<> where [] {} + impl FooTrait<> for T where [T: CoreTrait<>] {} + 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 { - safe trait CoreTrait<> where [] {} + trait CoreTrait<> where [] {} struct CoreStruct<> where [] {} - safe impl<> !CoreTrait<> for CoreStruct<> where [] {} + impl<> !CoreTrait<> for CoreStruct<> where [] {} }, crate foo { - safe trait FooTrait<> where [] {} - safe impl FooTrait<> for T where [T: CoreTrait<>] {} - safe impl<> FooTrait<> for CoreStruct<> where [] {} + trait FooTrait<> where [] {} + impl FooTrait<> for T where [T: CoreTrait<>] {} + 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 { - safe trait Iterator<> where [] { + trait Iterator<> where [] { } - safe trait Mirror<> where [] { + trait Mirror<> where [] { type T<> : [] where []; } - safe impl Mirror<> for A where [] { + impl Mirror<> for A where [] { type T<> = A where []; } struct LocalType<> where [] {} - safe trait LocalTrait<> where [] { } + trait LocalTrait<> where [] { } - safe impl LocalTrait<> for T where [T: Iterator<>] { } + impl LocalTrait<> for T where [T: Iterator<>] { } - safe impl<> LocalTrait<> for ::T where [] { } + 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: `safe impl LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs `safe 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("safe impl<> Iterator<> for LocalType<> where [] {}"))); + .assert_debug_eq(&test_program_ok(&gen_program("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 { - safe trait Iterator<> where [] { + trait Iterator<> where [] { } - safe trait Mirror<> where [] { + trait Mirror<> where [] { type T<> : [] where []; } - safe impl Mirror<> for A where [] { + impl Mirror<> for A where [] { type T<> = A where []; } struct LocalType<> where [] {} - safe trait LocalTrait<> where [] { } + trait LocalTrait<> where [] { } - safe impl LocalTrait<> for T where [T: Iterator<>] { } + impl LocalTrait<> for T where [T: Iterator<>] { } - safe impl LocalTrait<> for ::T where [T: Mirror<>] { } + 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: `safe impl LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs `safe 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( - "safe impl<> Iterator<> for u32 where[] {}", + "impl<> Iterator<> for u32 where[] {}", ))); } diff --git a/tests/hello_world.rs b/tests/hello_world.rs index e2cd7ca5..1865d578 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 { - safe trait Foo where [T: Bar] {} + trait Foo where [T: Bar] {} - safe trait Bar where [T: Baz<>] {} + trait Bar where [T: Baz<>] {} - safe trait Baz<> where [] {} + trait Baz<> where [] {} } ]", )); @@ -32,11 +32,11 @@ fn test_ok() { .assert_debug_eq(&test_program_ok( "[ crate Foo { - safe trait Foo where [T: Bar, Self: Baz<>] {} + trait Foo where [T: Bar, Self: Baz<>] {} - safe trait Bar where [T: Baz<>] {} + trait Bar where [T: Baz<>] {} - safe trait Baz<> where [] {} + trait Baz<> where [] {} } ]", )); diff --git a/tests/unsafe-trait.rs b/tests/unsafe-trait.rs index 2b6626fb..3a7dbf11 100644 --- a/tests/unsafe-trait.rs +++ b/tests/unsafe-trait.rs @@ -5,7 +5,7 @@ fn unsafe_trait_requires_unsafe_impl_err() { expect_test::expect![[r#" Err( Error { - context: "check_trait_impl(safe impl <> SendTrait < > for (rigid (adt SendStruct)) where [] { })", + context: "check_trait_impl(Safe impl <> SendTrait < > for (rigid (adt SendStruct)) where [] { })", source: "the trait requires an `unsafe impl` declaration", }, ) @@ -15,7 +15,7 @@ fn unsafe_trait_requires_unsafe_impl_err() { crate core { unsafe trait SendTrait<> where [] {} struct SendStruct<> where [] {} - safe impl<> SendTrait<> for SendStruct<> where [] {} + impl<> SendTrait<> for SendStruct<> where [] {} } ]", )); From b2af5297ba8af0e97bbf966901934f6b6ea70a02 Mon Sep 17 00:00:00 2001 From: Yosh Date: Thu, 29 Jun 2023 12:03:16 +0200 Subject: [PATCH 6/6] remove `Safe` annotation from error messages --- crates/formality-prove/src/decls.rs | 13 ++++++++++++- tests/coherence_orphan.rs | 10 +++++----- tests/coherence_overlap.rs | 16 ++++++++-------- tests/unsafe-trait.rs | 2 +- 4 files changed, 26 insertions(+), 15 deletions(-) diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 78ebb817..1fafa26b 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -125,12 +125,23 @@ pub struct NegImplDeclBoundData { } /// Mark a trait or trait impl as `unsafe`. -#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum Safety { Safe, Unsafe, } +// NOTE(yosh): `Debug` is currently used to print error messages with. In order +// to not print `safe impl` / `safe trait` where none is written, we leave the impl blank. +impl std::fmt::Debug for Safety { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Self::Safe => write!(f, ""), + Self::Unsafe => write!(f, "unsafe"), + } + } +} + impl Term for Safety {} impl DowncastTo for Safety { diff --git a/tests/coherence_orphan.rs b/tests/coherence_orphan.rs index c7d78c77..1af9efaf 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(Safe impl <> CoreTrait < > for (rigid (adt CoreStruct)) where [] { })", + context: "orphan_check( impl <> CoreTrait < > for (rigid (adt CoreStruct)) where [] { })", source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}", }, ) @@ -31,7 +31,7 @@ fn test_orphan_neg_CoreTrait_for_CoreStruct_in_Foo() { expect_test::expect![[r#" Err( Error { - context: "orphan_check_neg(Safe impl <> ! CoreTrait < > for (rigid (adt CoreStruct)) where [] {})", + context: "orphan_check_neg( impl <> ! CoreTrait < > for (rigid (adt CoreStruct)) where [] {})", source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}", }, ) @@ -54,7 +54,7 @@ fn test_orphan_mirror_CoreStruct() { expect_test::expect![[r#" Err( Error { - context: "orphan_check(Safe impl <> CoreTrait < > for (alias (Mirror :: Assoc) (rigid (adt CoreStruct))) where [] { })", + context: "orphan_check( impl <> CoreTrait < > for (alias (Mirror :: Assoc) (rigid (adt CoreStruct))) where [] { })", source: "failed to prove {@ IsLocal(CoreTrait((alias (Mirror :: Assoc) (rigid (adt CoreStruct)))))} given {}, got {}", }, ) @@ -119,7 +119,7 @@ fn test_orphan_alias_to_unit() { expect_test::expect![[r#" Err( Error { - context: "orphan_check(Safe impl <> CoreTrait < > for (alias (Unit :: Assoc) (rigid (adt FooStruct))) where [] { })", + context: "orphan_check( impl <> CoreTrait < > for (alias (Unit :: Assoc) (rigid (adt FooStruct))) where [] { })", source: "failed to prove {@ IsLocal(CoreTrait((alias (Unit :: Assoc) (rigid (adt FooStruct)))))} given {}, got {}", }, ) @@ -150,7 +150,7 @@ fn test_orphan_uncovered_T() { expect_test::expect![[r#" Err( Error { - context: "orphan_check(Safe impl CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { })", + context: "orphan_check( impl CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { })", source: "failed to prove {@ IsLocal(CoreTrait(!ty_1, (rigid (adt FooStruct))))} given {}, got {}", }, ) diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs index 98a50f1e..90cfc703 100644 --- a/tests/coherence_overlap.rs +++ b/tests/coherence_overlap.rs @@ -27,7 +27,7 @@ fn test_u32_u32_impls() { // Test that we detect duplicate impls. expect_test::expect![[r#" Err( - "duplicate impl in current crate: Safe impl <> Foo < > for (rigid (scalar u32)) where [] { }", + "duplicate impl in current crate: impl <> Foo < > for (rigid (scalar u32)) where [] { }", ) "#]] .assert_debug_eq(&test_program_ok( @@ -46,7 +46,7 @@ fn test_u32_T_impls() { // Test that we detect overlap involving generic parameters. expect_test::expect![[r#" Err( - "impls may overlap: `Safe impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `Safe impl Foo < > for ^ty0_0 where [] { }`", + "impls may overlap: ` impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs ` impl Foo < > for ^ty0_0 where [] { }`", ) "#]] .assert_debug_eq(&test_program_ok( @@ -90,7 +90,7 @@ fn test_u32_T_where_T_Is_impls() { // and also all `T: Is`, and `u32: Is`. expect_test::expect![[r#" Err( - "impls may overlap: `Safe impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs `Safe impl Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`", + "impls may overlap: ` impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs ` impl Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`", ) "#]] .assert_debug_eq(&test_program_ok( @@ -113,7 +113,7 @@ fn test_u32_not_u32_impls() { expect_test::expect![[r#" Err( Error { - context: "check_trait_impl(Safe impl <> Foo < > for (rigid (scalar u32)) where [] { })", + context: "check_trait_impl( 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: {} }}", }, ) @@ -139,7 +139,7 @@ fn test_T_where_Foo_not_u32_impls() { expect_test::expect![[r#" Err( Error { - context: "check_trait_impl(Safe impl Foo < > for ^ty0_0 where [^ty0_0 : Foo < >] { })", + context: "check_trait_impl( 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))} }}", }, ) @@ -159,7 +159,7 @@ 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: `Safe impl FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs `Safe impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`", + "impls may overlap: ` impl FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs ` impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`", ) "#]] .assert_debug_eq(&test_program_ok( @@ -253,7 +253,7 @@ fn test_overlap_normalize_alias_to_LocalType() { expect_test::expect![[r#" Err( - "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 [] { }`", + "impls may overlap: ` impl LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs ` impl <> LocalTrait < > for (alias (Mirror :: T) (rigid (adt LocalType))) where [] { }`", ) "#]] .assert_debug_eq(&test_program_ok(&gen_program("impl<> Iterator<> for LocalType<> where [] {}"))); @@ -312,7 +312,7 @@ fn test_overlap_alias_not_normalizable() { expect_test::expect![[r#" Err( - "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 < >] { }`", + "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 < >] { }`", ) "#]] // FIXME .assert_debug_eq(&test_program_ok(&gen_program( diff --git a/tests/unsafe-trait.rs b/tests/unsafe-trait.rs index 3a7dbf11..fe335eb0 100644 --- a/tests/unsafe-trait.rs +++ b/tests/unsafe-trait.rs @@ -5,7 +5,7 @@ fn unsafe_trait_requires_unsafe_impl_err() { expect_test::expect![[r#" Err( Error { - context: "check_trait_impl(Safe impl <> SendTrait < > for (rigid (adt SendStruct)) where [] { })", + context: "check_trait_impl( impl <> SendTrait < > for (rigid (adt SendStruct)) where [] { })", source: "the trait requires an `unsafe impl` declaration", }, )