Skip to content

Commit

Permalink
implement safety check for negative impls
Browse files Browse the repository at this point in the history
  • Loading branch information
lqd committed Nov 11, 2023
1 parent 20787fd commit 519e4da
Showing 1 changed file with 8 additions and 2 deletions.
10 changes: 8 additions & 2 deletions crates/formality-check/src/impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -52,18 +52,24 @@ impl super::Check<'_> {
Ok(())
}

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

let NegTraitImplBoundData {
trait_id,
self_ty,
trait_parameters,
where_clauses,
} = env.instantiate_universally(&i.binder);
} = env.instantiate_universally(&trait_impl.binder);

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

// Negative impls are always safe (rustc E0198) regardless of the trait's safety.
if trait_impl.safety == Safety::Unsafe {
bail!("negative impls cannot be unsafe");
}

self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;

self.prove_goal(&env, &where_clauses, trait_ref.not_implemented())?;
Expand Down

0 comments on commit 519e4da

Please sign in to comment.