Implement unsafe trait support #128
Conversation
yoshuawuyts
force-pushed
the
unsafe-traits
branch
from
91fb04d
to
8936842
Compare
|
I've instead hand-rolled the parser, removing the need for |
crates/formality-prove/src/decls.rs
Outdated
| @@ -117,8 +119,15 @@ pub struct NegImplDeclBoundData { | |||
| pub where_clause: Wcs, | |||
| } | |||
|
|
|||
| #[term(trait $id $binder)] | |||
| #[term] | |||
There was a problem hiding this comment.
Hmm, so if we wanted to do
trait Foo { }vs
unsafe trait foo { }we have two ways to do it:
- Implement the parsing traits manually for
Safety - Or extend the procedural macro to accommodate this case
I'm inclined to do the latter, as I think it will come up. Something like setting a "default" variant.
There was a problem hiding this comment.
I'm inclined to do the latter, as I think it will come up. Something like setting a "default" variant.
I think that's reasonable; I honestly don't love the custom parsing strategy I took in this PR, and I'm happy to instead change the proc macro.
crates/formality-prove/src/decls.rs
Outdated
| #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] | ||
| pub enum Safety { | ||
| Safe, | ||
| Unsafe, | ||
| } |
There was a problem hiding this comment.
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
safeandunsafebut 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.
There was a problem hiding this comment.
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!
|
What do you think about this question, @yoshuawuyts ? |
There was a problem hiding this comment.
Hmm, this is exposing a shortcoming of the pretty printer, but it's not obvious to me how to fix it. Ideally we'd skip the separator if the field before printed nothing, but it's kind of tricky to know when that might be true. Well, we could generate a String and then check its length...? Anyway, I guess that's a distinct PR. =) The code to modify would be in debug.rs. I looked though and didn't see a tiny diff that would work.
| @@ -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( impl <> ! CoreTrait < > for (rigid (adt CoreStruct)) where [] {})", | |||
There was a problem hiding this comment.
hmm this is annoying :)
|
I think I started to lay the groundwork to handle this nicely now. We have |
|
I think I should probably throw in the towel on this patch for now; I currently don't have the bandwidth to see this through. If someone wants to take this over please feel free to run with this. Happy to close this if that's preferred too. |
|
@lqd said they were up for it |
|
Closing in favor of #155 |
Closes #50. This implements support for
unsafe traitandunsafe impl. However, I'm not yet super comfortable with the parser - so I've implemented it using an enum which means that non-unsafe trait decls and impls are now written:safe traitandsafe implrespectively.Is the right approach to instead manually implement the
Parsertrait? I have a feeling that the MIR syntax is intended to be unambiguous, so is that even something we want to do? Or should every trait decl and impl be explicit about whether it's unsafe or not? Any guidance here would be appreciated!Best reviewed one commit at a time