@@ -6,8 +6,8 @@ use formality_prove::{Env, Safety};
6
6
use formality_rust:: {
7
7
grammar:: {
8
8
AssociatedTy , AssociatedTyBoundData , AssociatedTyValue , AssociatedTyValueBoundData , Fn ,
9
- FnBoundData , ImplItem , NegTraitImpl , NegTraitImplBoundData , TraitBoundData , TraitImpl ,
10
- TraitImplBoundData , TraitItem ,
9
+ FnBoundData , ImplItem , NegTraitImpl , NegTraitImplBoundData , Trait , TraitBoundData ,
10
+ TraitImpl , TraitImplBoundData , TraitItem ,
11
11
} ,
12
12
prove:: ToWcs ,
13
13
} ;
@@ -45,7 +45,7 @@ impl super::Check<'_> {
45
45
trait_items,
46
46
} = trait_decl. binder . instantiate_with ( & trait_ref. parameters ) ?;
47
47
48
- self . check_safety_matches ( & trait_decl. safety , safety) ?;
48
+ self . check_safety_matches ( & trait_decl, safety) ?;
49
49
50
50
for impl_item in & impl_items {
51
51
self . check_trait_impl_item ( & env, & where_clauses, & trait_items, impl_item) ?;
@@ -73,17 +73,16 @@ impl super::Check<'_> {
73
73
Ok ( ( ) )
74
74
}
75
75
76
- /// Validate `unsafe trait` and `unsafe impl` line up
77
- fn check_safety_matches ( & self , trait_decl : & Safety , trait_impl : & Safety ) -> Fallible < ( ) > {
78
- match trait_decl {
79
- Safety :: Safe => anyhow:: ensure!(
80
- matches!( trait_impl, Safety :: Safe ) ,
81
- "implementing the trait is not `unsafe`"
82
- ) ,
83
- Safety :: Unsafe => anyhow:: ensure!(
84
- matches!( trait_impl, Safety :: Unsafe ) ,
85
- "the trait requires an `unsafe impl` declaration"
86
- ) ,
76
+ /// Validate that the declared safety of an impl matches the one from the trait declaration.
77
+ fn check_safety_matches ( & self , trait_decl : & Trait , trait_impl : & Safety ) -> Fallible < ( ) > {
78
+ if trait_decl. safety != * trait_impl {
79
+ match trait_decl. safety {
80
+ Safety :: Safe => bail ! ( "implementing the trait `{:?}` is not unsafe" , trait_decl. id) ,
81
+ Safety :: Unsafe => bail ! (
82
+ "the trait `{:?}` requires an `unsafe impl` declaration" ,
83
+ trait_decl. id
84
+ ) ,
85
+ }
87
86
}
88
87
Ok ( ( ) )
89
88
}
0 commit comments