Skip to content

Commit ddbb916

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #155 from lqd/unsafe-traits
Implement unsafe trait support (continued)
2 parents b7fd961 + 53d0e43 commit ddbb916

22 files changed

+161
-27
lines changed

‎crates/formality-check/src/impls.rs‎

Lines changed: 30 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ use anyhow::bail;
22

33
use fn_error_context::context;
44
use formality_core::Downcasted;
5-
use formality_prove::Env;
5+
use formality_prove::{Env, Safety};
66
use formality_rust::{
77
grammar::{
88
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,
1111
},
1212
prove::ToWcs,
1313
};
@@ -17,10 +17,8 @@ use formality_types::{
1717
};
1818

1919
impl super::Check<'_> {
20-
#[context("check_trait_impl({v:?})")]
21-
pub(super) fn check_trait_impl(&self, v: &TraitImpl) -> Fallible<()> {
22-
let TraitImpl { binder } = v;
23-
20+
#[context("check_trait_impl({trait_impl:?})")]
21+
pub(super) fn check_trait_impl(&self, trait_impl: &TraitImpl) -> Fallible<()> {
2422
let mut env = Env::default();
2523

2624
let TraitImplBoundData {
@@ -29,7 +27,7 @@ impl super::Check<'_> {
2927
trait_parameters,
3028
where_clauses,
3129
impl_items,
32-
} = env.instantiate_universally(binder);
30+
} = env.instantiate_universally(&trait_impl.binder);
3331

3432
let trait_ref = trait_id.with(self_ty, trait_parameters);
3533

@@ -45,32 +43,54 @@ impl super::Check<'_> {
4543
trait_items,
4644
} = trait_decl.binder.instantiate_with(&trait_ref.parameters)?;
4745

46+
self.check_safety_matches(&trait_decl, &trait_impl)?;
47+
4848
for impl_item in &impl_items {
4949
self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?;
5050
}
5151

5252
Ok(())
5353
}
5454

55-
pub(super) fn check_neg_trait_impl(&self, i: &NegTraitImpl) -> Fallible<()> {
55+
#[context("check_neg_trait_impl({trait_impl:?})")]
56+
pub(super) fn check_neg_trait_impl(&self, trait_impl: &NegTraitImpl) -> Fallible<()> {
5657
let mut env = Env::default();
5758

5859
let NegTraitImplBoundData {
5960
trait_id,
6061
self_ty,
6162
trait_parameters,
6263
where_clauses,
63-
} = env.instantiate_universally(&i.binder);
64+
} = env.instantiate_universally(&trait_impl.binder);
6465

6566
let trait_ref = trait_id.with(self_ty, trait_parameters);
6667

68+
// Negative impls are always safe (rustc E0198) regardless of the trait's safety.
69+
if trait_impl.safety == Safety::Unsafe {
70+
bail!("negative impls cannot be unsafe");
71+
}
72+
6773
self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;
6874

6975
self.prove_goal(&env, &where_clauses, trait_ref.not_implemented())?;
7076

7177
Ok(())
7278
}
7379

80+
/// Validate that the declared safety of an impl matches the one from the trait declaration.
81+
fn check_safety_matches(&self, trait_decl: &Trait, trait_impl: &TraitImpl) -> Fallible<()> {
82+
if trait_decl.safety != trait_impl.safety {
83+
match trait_decl.safety {
84+
Safety::Safe => bail!("implementing the trait `{:?}` is not unsafe", trait_decl.id),
85+
Safety::Unsafe => bail!(
86+
"the trait `{:?}` requires an `unsafe impl` declaration",
87+
trait_decl.id
88+
),
89+
}
90+
}
91+
Ok(())
92+
}
93+
7494
fn check_trait_impl_item(
7595
&self,
7696
env: &Env,

‎crates/formality-check/src/traits.rs‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,11 @@ use formality_types::grammar::Fallible;
88
impl super::Check<'_> {
99
#[context("check_trait({:?})", t.id)]
1010
pub(super) fn check_trait(&self, t: &Trait) -> Fallible<()> {
11-
let Trait { id: _, binder } = t;
11+
let Trait {
12+
safety: _,
13+
id: _,
14+
binder,
15+
} = t;
1216
let mut env = Env::default();
1317

1418
let TraitBoundData {

‎crates/formality-core/src/judgment/test_filtered.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
#![cfg(test)]
22

33
use std::sync::Arc;
4-
use crate::cast_impl;
54

5+
use crate::cast_impl;
66
use crate::judgment_fn;
77

88
#[derive(Ord, PartialOrd, Eq, PartialEq, Clone, Debug, Hash)]
@@ -24,14 +24,14 @@ impl Graph {
2424
judgment_fn!(
2525
fn transitive_reachable(g: Arc<Graph>, node: u32) => u32 {
2626
debug(node, g)
27-
27+
2828
(
2929
(graph.successors(a) => b)
3030
(if b % 2 == 0)
3131
--------------------------------------- ("base")
3232
(transitive_reachable(graph, a) => b)
3333
)
34-
34+
3535
(
3636
(transitive_reachable(&graph, a) => b)
3737
(transitive_reachable(&graph, b) => c)

‎crates/formality-macros/src/debug.rs‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -242,14 +242,24 @@ fn debug_variant_with_attr(
242242

243243
fn debug_field_with_mode(name: &Ident, mode: &FieldMode) -> TokenStream {
244244
match mode {
245-
FieldMode::Single | FieldMode::Optional => {
245+
FieldMode::Single => {
246246
quote_spanned! { name.span() =>
247247
write!(fmt, "{}", sep)?;
248248
write!(fmt, "{:?}", #name)?;
249249
sep = " ";
250250
}
251251
}
252252

253+
FieldMode::Optional => {
254+
quote_spanned! { name.span() =>
255+
if !::formality_core::util::is_default(#name) {
256+
write!(fmt, "{}", sep)?;
257+
write!(fmt, "{:?}", #name)?;
258+
sep = " ";
259+
}
260+
}
261+
}
262+
253263
FieldMode::Many => {
254264
quote_spanned! { name.span() =>
255265
for e in #name {

‎crates/formality-prove/src/db.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+

‎crates/formality-prove/src/decls.rs‎

Lines changed: 32 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
use std::fmt;
2+
13
use formality_core::{set, Set, Upcast};
24
use formality_macros::term;
35
use formality_types::grammar::{
@@ -104,8 +106,10 @@ impl Decls {
104106

105107
/// An "impl decl" indicates that a trait is implemented for a given set of types.
106108
/// One "impl decl" is created for each impl in the Rust source.
107-
#[term(impl $binder)]
109+
#[term($?safety impl $binder)]
108110
pub struct ImplDecl {
111+
/// The safety this impl declares, which needs to match the implemented trait's safety.
112+
pub safety: Safety,
109113
/// The binder covers the generic variables from the impl
110114
pub binder: Binder<ImplDeclBoundData>,
111115
}
@@ -122,8 +126,11 @@ pub struct ImplDeclBoundData {
122126

123127
/// A declaration that some trait will *not* be implemented for a type; derived from negative impls
124128
/// like `impl !Foo for Bar`.
125-
#[term(impl $binder)]
129+
#[term($?safety impl $binder)]
126130
pub struct NegImplDecl {
131+
/// The safety this negative impl declares
132+
pub safety: Safety,
133+
127134
/// Binder comes the generics on the impl
128135
pub binder: Binder<NegImplDeclBoundData>,
129136
}
@@ -135,15 +142,37 @@ pub struct NegImplDeclBoundData {
135142
pub where_clause: Wcs,
136143
}
137144

145+
/// Mark a trait or trait impl as `unsafe`.
146+
#[term]
147+
#[customize(debug)]
148+
#[derive(Default)]
149+
pub enum Safety {
150+
#[default]
151+
Safe,
152+
Unsafe,
153+
}
154+
155+
impl fmt::Debug for Safety {
156+
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
157+
match self {
158+
Safety::Safe => write!(f, "safe"),
159+
Safety::Unsafe => write!(f, "unsafe"),
160+
}
161+
}
162+
}
163+
138164
/// A "trait declaration" declares a trait that exists, its generics, and its where-clauses.
139165
/// It doesn't capture the trait items, which will be transformed into other sorts of rules.
140166
///
141167
/// In Rust syntax, it covers the `trait Foo: Bar` part of the declaration, but not what appears in the `{...}`.
142-
#[term(trait $id $binder)]
168+
#[term($?safety trait $id $binder)]
143169
pub struct TraitDecl {
144170
/// The name of the trait
145171
pub id: TraitId,
146172

173+
/// Whether the trait is `unsafe` or not
174+
pub safety: Safety,
175+
147176
/// The binder here captures the generics of the trait; it always begins with a `Self` type.
148177
pub binder: Binder<TraitDeclBoundData>,
149178
}

‎crates/formality-prove/src/prove/minimize/test.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ fn minimize_a() {
2323
let (mut env_min, term_min, m) = minimize(env, term);
2424

2525
expect!["(Env { variables: [?ty_0, ?ty_1], coherence_mode: false }, [?ty_0, ?ty_1])"]
26-
.assert_eq(&format!("{:?}", (&env_min, &term_min)));
26+
.assert_eq(&format!("{:?}", (&env_min, &term_min)));
2727

2828
let ty0 = term_min[0].as_variable().unwrap();
2929
let ty1 = term_min[1].as_variable().unwrap();

‎crates/formality-rust/src/grammar.rs‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
use std::sync::Arc;
22

33
use formality_core::{term, Upcast};
4+
use formality_prove::Safety;
45
use formality_types::{
56
grammar::{
67
AdtId, AliasTy, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt,
@@ -160,8 +161,9 @@ pub struct Variant {
160161
pub fields: Vec<Field>,
161162
}
162163

163-
#[term(trait $id $binder)]
164+
#[term($?safety trait $id $binder)]
164165
pub struct Trait {
166+
pub safety: Safety,
165167
pub id: TraitId,
166168
pub binder: TraitBinder<TraitBoundData>,
167169
}
@@ -241,8 +243,9 @@ pub struct AssociatedTyBoundData {
241243
pub where_clauses: Vec<WhereClause>,
242244
}
243245

244-
#[term(impl $binder)]
246+
#[term($?safety impl $binder)]
245247
pub struct TraitImpl {
248+
pub safety: Safety,
246249
pub binder: Binder<TraitImplBoundData>,
247250
}
248251

@@ -267,8 +270,9 @@ impl TraitImplBoundData {
267270
}
268271
}
269272

270-
#[term(impl $binder)]
273+
#[term($?safety impl $binder)]
271274
pub struct NegTraitImpl {
275+
pub safety: Safety,
272276
pub binder: Binder<NegTraitImplBoundData>,
273277
}
274278

‎crates/formality-rust/src/prove.rs‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ impl Crate {
8080
self.items
8181
.iter()
8282
.flat_map(|item| match item {
83-
CrateItem::Trait(Trait { id, binder }) => {
83+
CrateItem::Trait(Trait { id, binder, safety }) => {
8484
let (
8585
vars,
8686
TraitBoundData {
@@ -89,6 +89,7 @@ impl Crate {
8989
},
9090
) = binder.open();
9191
Some(prove::TraitDecl {
92+
safety: safety.clone(),
9293
id: id.clone(),
9394
binder: Binder::new(
9495
vars,
@@ -110,7 +111,7 @@ impl Crate {
110111
self.items
111112
.iter()
112113
.flat_map(|item| match item {
113-
CrateItem::TraitImpl(TraitImpl { binder }) => {
114+
CrateItem::TraitImpl(TraitImpl { binder, safety }) => {
114115
let (
115116
vars,
116117
TraitImplBoundData {
@@ -122,6 +123,7 @@ impl Crate {
122123
},
123124
) = binder.open();
124125
Some(prove::ImplDecl {
126+
safety: safety.clone(),
125127
binder: Binder::new(
126128
vars,
127129
prove::ImplDeclBoundData {
@@ -140,7 +142,7 @@ impl Crate {
140142
self.items
141143
.iter()
142144
.flat_map(|item| match item {
143-
CrateItem::NegTraitImpl(NegTraitImpl { binder }) => {
145+
CrateItem::NegTraitImpl(NegTraitImpl { binder, safety }) => {
144146
let (
145147
vars,
146148
NegTraitImplBoundData {
@@ -151,6 +153,7 @@ impl Crate {
151153
},
152154
) = binder.open();
153155
Some(prove::NegImplDecl {
156+
safety: safety.clone(),
154157
binder: Binder::new(
155158
vars,
156159
prove::NegImplDeclBoundData {
@@ -169,7 +172,7 @@ impl Crate {
169172
self.items
170173
.iter()
171174
.flat_map(|item| match item {
172-
CrateItem::TraitImpl(TraitImpl { binder }) => {
175+
CrateItem::TraitImpl(TraitImpl { binder, safety: _ }) => {
173176
let (
174177
impl_vars,
175178
TraitImplBoundData {
@@ -226,6 +229,7 @@ impl Crate {
226229
.iter()
227230
.flat_map(|item| match item {
228231
CrateItem::Trait(Trait {
232+
safety: _,
229233
id: trait_id,
230234
binder,
231235
}) => {

‎examples/formality-eg/type_system.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+

0 commit comments

Comments
 (0)