Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement unsafe trait support #128

Closed
wants to merge 6 commits into from
Closed

Implement unsafe trait support #128

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
0c78cd6
add failing unsafe traits test
yoshuawuyts Jun 28, 2023
7e83206
implement `unsafe trait` support
yoshuawuyts Jun 29, 2023
8936842
update trait {decls,impls} with a `safe` prefix
yoshuawuyts Jun 29, 2023
7767395
hand-roll parser for `enum Safety`
yoshuawuyts Jun 29, 2023
4a6523f
remove the `safe trait` notation
yoshuawuyts Jun 29, 2023
b2af529
remove `Safe` annotation from error messages
yoshuawuyts Jun 29, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion crates/formality-prove/src/decls.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you could get this same effect with

#[term]
pub enum Safety {
    #[grammar()]
    Safe,
    #[grammar(unsafe)]
    Unsafe,
}

That said, I didn't recommend it earlier because I thought we probably wanted to keep safe in the debug output. I'm torn between:

  • Accept (and print) both safe and unsafe but have a default when parsing -- what I was originally thinking
  • Never print safe -- wht you are doing

The former seems more explicit and clear, but it departs a bit from Rust surface syntax. I still think that's the way to go though, we do similar things in a few other places. I do think it's important to not require users to write safe trait in tests though.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, I agree that that seems like the way to go. I initially had safe trait Foo-notation everywhere, and that felt really clumsy. But just having it as part of debug output seems like it would be good!


// 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<Self> for Safety {
Expand Down
10 changes: 5 additions & 5 deletions tests/coherence_orphan.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {}",
},
)
Expand All @@ -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 [] {})",
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hmm this is annoying :)

source: "failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}",
},
)
Expand All @@ -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 {}",
},
)
Expand Down Expand Up @@ -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 {}",
},
)
Expand Down Expand Up @@ -150,7 +150,7 @@ fn test_orphan_uncovered_T() {
expect_test::expect![[r#"
Err(
Error {
context: "orphan_check(Safe impl <ty> CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { })",
context: "orphan_check( impl <ty> CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { })",
source: "failed to prove {@ IsLocal(CoreTrait(!ty_1, (rigid (adt FooStruct))))} given {}, got {}",
},
)
Expand Down
16 changes: 8 additions & 8 deletions tests/coherence_overlap.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -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 <ty> Foo < > for ^ty0_0 where [] { }`",
"impls may overlap: ` impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs ` impl <ty> Foo < > for ^ty0_0 where [] { }`",
)
"#]]
.assert_debug_eq(&test_program_ok(
Expand Down Expand Up @@ -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 <ty> Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`",
"impls may overlap: ` impl <> Foo < > for (rigid (scalar u32)) where [] { }` vs ` impl <ty> Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }`",
)
"#]]
.assert_debug_eq(&test_program_ok(
Expand All @@ -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: {} }}",
},
)
Expand All @@ -139,7 +139,7 @@ fn test_T_where_Foo_not_u32_impls() {
expect_test::expect![[r#"
Err(
Error {
context: "check_trait_impl(Safe impl <ty> Foo < > for ^ty0_0 where [^ty0_0 : Foo < >] { })",
context: "check_trait_impl( impl <ty> 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))} }}",
},
)
Expand All @@ -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 <ty> FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs `Safe impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`",
"impls may overlap: ` impl <ty> FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }` vs ` impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }`",
)
"#]]
.assert_debug_eq(&test_program_ok(
Expand Down Expand Up @@ -253,7 +253,7 @@ fn test_overlap_normalize_alias_to_LocalType() {

expect_test::expect![[r#"
Err(
"impls may overlap: `Safe impl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs `Safe impl <> LocalTrait < > for (alias (Mirror :: T) (rigid (adt LocalType))) where [] { }`",
"impls may overlap: ` impl <ty> 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 [] {}")));
Expand Down Expand Up @@ -312,7 +312,7 @@ fn test_overlap_alias_not_normalizable() {

expect_test::expect![[r#"
Err(
"impls may overlap: `Safe impl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs `Safe impl <ty> LocalTrait < > for (alias (Mirror :: T) ^ty0_0) where [^ty0_0 : Mirror < >] { }`",
"impls may overlap: ` impl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }` vs ` impl <ty> LocalTrait < > for (alias (Mirror :: T) ^ty0_0) where [^ty0_0 : Mirror < >] { }`",
)
"#]] // FIXME
.assert_debug_eq(&test_program_ok(&gen_program(
Expand Down
2 changes: 1 addition & 1 deletion tests/unsafe-trait.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
},
)
Expand Down