From 570e95f733a52bd7db607b77be32cff7cc388e6b Mon Sep 17 00:00:00 2001
From: Yosh <github@yosh.is>
Date: Thu, 29 Jun 2023 02:16:55 +0200
Subject: [PATCH 01/11] implement `unsafe trait` support

---
 crates/formality-check/src/impls.rs  | 21 +++++++++++++++++++--
 crates/formality-check/src/traits.rs |  6 +++++-
 crates/formality-prove/src/decls.rs  | 22 +++++++++++++++++++---
 crates/formality-rust/src/grammar.rs | 10 +++++++---
 crates/formality-rust/src/prove.rs   | 12 ++++++++----
 5 files changed, 58 insertions(+), 13 deletions(-)

diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
index a8e04a03..43fe28e1 100644
--- a/crates/formality-check/src/impls.rs
+++ b/crates/formality-check/src/impls.rs
@@ -2,7 +2,7 @@ use anyhow::bail;
 
 use fn_error_context::context;
 use formality_core::Downcasted;
-use formality_prove::Env;
+use formality_prove::{Env, Safety};
 use formality_rust::{
     grammar::{
         AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Fn,
@@ -19,7 +19,7 @@ use formality_types::{
 impl super::Check<'_> {
     #[context("check_trait_impl({v:?})")]
     pub(super) fn check_trait_impl(&self, v: &TraitImpl) -> Fallible<()> {
-        let TraitImpl { binder } = v;
+        let TraitImpl { binder, safety } = v;
 
         let mut env = Env::default();
 
@@ -45,6 +45,8 @@ impl super::Check<'_> {
             trait_items,
         } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?;
 
+        self.check_safety_matches(&trait_decl.safety, safety)?;
+
         for impl_item in &impl_items {
             self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?;
         }
@@ -71,6 +73,21 @@ impl super::Check<'_> {
         Ok(())
     }
 
+    /// Validate `unsafe trait` and `unsafe impl` line up
+    fn check_safety_matches(&self, trait_decl: &Safety, trait_impl: &Safety) -> Fallible<()> {
+        match trait_decl {
+            Safety::Safe => anyhow::ensure!(
+                matches!(trait_impl, Safety::Safe),
+                "implementing the trait is not `unsafe`"
+            ),
+            Safety::Unsafe => anyhow::ensure!(
+                matches!(trait_impl, Safety::Unsafe),
+                "the trait requires an `unsafe impl` declaration"
+            ),
+        }
+        Ok(())
+    }
+
     fn check_trait_impl_item(
         &self,
         env: &Env,
diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs
index 1347ce92..22791031 100644
--- a/crates/formality-check/src/traits.rs
+++ b/crates/formality-check/src/traits.rs
@@ -8,7 +8,11 @@ use formality_types::grammar::Fallible;
 impl super::Check<'_> {
     #[context("check_trait({:?})", t.id)]
     pub(super) fn check_trait(&self, t: &Trait) -> Fallible<()> {
-        let Trait { id: _, binder } = t;
+        let Trait {
+            safety: _,
+            id: _,
+            binder,
+        } = t;
         let mut env = Env::default();
 
         let TraitBoundData {
diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs
index 38307b36..25e7aa64 100644
--- a/crates/formality-prove/src/decls.rs
+++ b/crates/formality-prove/src/decls.rs
@@ -104,8 +104,10 @@ impl Decls {
 
 /// An "impl decl" indicates that a trait is implemented for a given set of types.
 /// One "impl decl" is created for each impl in the Rust source.
-#[term(impl $binder)]
+#[term($?safety impl $binder)]
 pub struct ImplDecl {
+    /// The safety this impl declares, which needs to match the implemented trait's safety.
+    pub safety: Safety,
     /// The binder covers the generic variables from the impl
     pub binder: Binder<ImplDeclBoundData>,
 }
@@ -122,8 +124,11 @@ pub struct ImplDeclBoundData {
 
 /// A declaration that some trait will *not* be implemented for a type; derived from negative impls
 /// like `impl !Foo for Bar`.
-#[term(impl $binder)]
+#[term($?safety impl $binder)]
 pub struct NegImplDecl {
+    /// The safety this negative impl declares
+    pub safety: Safety,
+
     /// Binder comes the generics on the impl
     pub binder: Binder<NegImplDeclBoundData>,
 }
@@ -135,15 +140,26 @@ pub struct NegImplDeclBoundData {
     pub where_clause: Wcs,
 }
 
+#[term]
+#[derive(Default)]
+pub enum Safety {
+    #[default]
+    Safe,
+    Unsafe,
+}
+
 /// A "trait declaration" declares a trait that exists, its generics, and its where-clauses.
 /// It doesn't capture the trait items, which will be transformed into other sorts of rules.
 ///
 /// In Rust syntax, it covers the `trait Foo: Bar` part of the declaration, but not what appears in the `{...}`.
-#[term(trait $id $binder)]
+#[term($?safety trait $id $binder)]
 pub struct TraitDecl {
     /// The name of the trait
     pub id: TraitId,
 
+    /// Whether the trait is `unsafe` or not
+    pub safety: Safety,
+
     /// The binder here captures the generics of the trait; it always begins with a `Self` type.
     pub binder: Binder<TraitDeclBoundData>,
 }
diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs
index f36f52f9..69ec1ba6 100644
--- a/crates/formality-rust/src/grammar.rs
+++ b/crates/formality-rust/src/grammar.rs
@@ -1,6 +1,7 @@
 use std::sync::Arc;
 
 use formality_core::{term, Upcast};
+use formality_prove::Safety;
 use formality_types::{
     grammar::{
         AdtId, AliasTy, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt,
@@ -160,8 +161,9 @@ pub struct Variant {
     pub fields: Vec<Field>,
 }
 
-#[term(trait $id $binder)]
+#[term($?safety trait $id $binder)]
 pub struct Trait {
+    pub safety: Safety,
     pub id: TraitId,
     pub binder: TraitBinder<TraitBoundData>,
 }
@@ -241,8 +243,9 @@ pub struct AssociatedTyBoundData {
     pub where_clauses: Vec<WhereClause>,
 }
 
-#[term(impl $binder)]
+#[term($?safety impl $binder)]
 pub struct TraitImpl {
+    pub safety: Safety,
     pub binder: Binder<TraitImplBoundData>,
 }
 
@@ -267,8 +270,9 @@ impl TraitImplBoundData {
     }
 }
 
-#[term(impl $binder)]
+#[term($?safety impl $binder)]
 pub struct NegTraitImpl {
+    pub safety: Safety,
     pub binder: Binder<NegTraitImplBoundData>,
 }
 
diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs
index f7bc8996..6224e894 100644
--- a/crates/formality-rust/src/prove.rs
+++ b/crates/formality-rust/src/prove.rs
@@ -80,7 +80,7 @@ impl Crate {
         self.items
             .iter()
             .flat_map(|item| match item {
-                CrateItem::Trait(Trait { id, binder }) => {
+                CrateItem::Trait(Trait { id, binder, safety }) => {
                     let (
                         vars,
                         TraitBoundData {
@@ -89,6 +89,7 @@ impl Crate {
                         },
                     ) = binder.open();
                     Some(prove::TraitDecl {
+                        safety: safety.clone(),
                         id: id.clone(),
                         binder: Binder::new(
                             vars,
@@ -110,7 +111,7 @@ impl Crate {
         self.items
             .iter()
             .flat_map(|item| match item {
-                CrateItem::TraitImpl(TraitImpl { binder }) => {
+                CrateItem::TraitImpl(TraitImpl { binder, safety }) => {
                     let (
                         vars,
                         TraitImplBoundData {
@@ -122,6 +123,7 @@ impl Crate {
                         },
                     ) = binder.open();
                     Some(prove::ImplDecl {
+                        safety: safety.clone(),
                         binder: Binder::new(
                             vars,
                             prove::ImplDeclBoundData {
@@ -140,7 +142,7 @@ impl Crate {
         self.items
             .iter()
             .flat_map(|item| match item {
-                CrateItem::NegTraitImpl(NegTraitImpl { binder }) => {
+                CrateItem::NegTraitImpl(NegTraitImpl { binder, safety }) => {
                     let (
                         vars,
                         NegTraitImplBoundData {
@@ -151,6 +153,7 @@ impl Crate {
                         },
                     ) = binder.open();
                     Some(prove::NegImplDecl {
+                        safety: safety.clone(),
                         binder: Binder::new(
                             vars,
                             prove::NegImplDeclBoundData {
@@ -169,7 +172,7 @@ impl Crate {
         self.items
             .iter()
             .flat_map(|item| match item {
-                CrateItem::TraitImpl(TraitImpl { binder }) => {
+                CrateItem::TraitImpl(TraitImpl { binder, safety: _ }) => {
                     let (
                         impl_vars,
                         TraitImplBoundData {
@@ -226,6 +229,7 @@ impl Crate {
             .iter()
             .flat_map(|item| match item {
                 CrateItem::Trait(Trait {
+                    safety: _,
                     id: trait_id,
                     binder,
                 }) => {

From c86992d905f63f7367bf36d33bd69137ece1cb10 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 11:01:49 +0000
Subject: [PATCH 02/11] add rustfmt to toolchain components

---
 rust-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rust-toolchain b/rust-toolchain
index 0a823a6e..c192ab89 100644
--- a/rust-toolchain
+++ b/rust-toolchain
@@ -1,3 +1,3 @@
 [toolchain]
 channel = "nightly-2023-10-08"
-components = [ "rustc-dev", "llvm-tools" ]
+components = ["rustc-dev", "llvm-tools", "rustfmt"]

From 8ec65895ffa32d96bf45017937f1f2d63ca4e0a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 11:03:46 +0000
Subject: [PATCH 03/11] fix spaces breaking rustfmt and format everything

---
 crates/formality-core/src/judgment/test_filtered.rs | 6 +++---
 crates/formality-prove/src/db.rs                    | 1 +
 crates/formality-prove/src/prove/minimize/test.rs   | 2 +-
 examples/formality-eg/type_system.rs                | 1 +
 4 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/crates/formality-core/src/judgment/test_filtered.rs b/crates/formality-core/src/judgment/test_filtered.rs
index d162c22a..d36f912d 100644
--- a/crates/formality-core/src/judgment/test_filtered.rs
+++ b/crates/formality-core/src/judgment/test_filtered.rs
@@ -1,8 +1,8 @@
 #![cfg(test)]
 
 use std::sync::Arc;
-use crate::cast_impl;
 
+use crate::cast_impl;
 use crate::judgment_fn;
 
 #[derive(Ord, PartialOrd, Eq, PartialEq, Clone, Debug, Hash)]
@@ -24,14 +24,14 @@ impl Graph {
 judgment_fn!(
     fn transitive_reachable(g: Arc<Graph>, node: u32) => u32 {
         debug(node, g)
-        
+
         (
             (graph.successors(a) => b)
             (if b % 2 == 0)
             --------------------------------------- ("base")
             (transitive_reachable(graph, a) => b)
         )
-    
+
         (
             (transitive_reachable(&graph, a) => b)
             (transitive_reachable(&graph, b) => c)
diff --git a/crates/formality-prove/src/db.rs b/crates/formality-prove/src/db.rs
index e69de29b..8b137891 100644
--- a/crates/formality-prove/src/db.rs
+++ b/crates/formality-prove/src/db.rs
@@ -0,0 +1 @@
+
diff --git a/crates/formality-prove/src/prove/minimize/test.rs b/crates/formality-prove/src/prove/minimize/test.rs
index a80688a2..c62e9e8f 100644
--- a/crates/formality-prove/src/prove/minimize/test.rs
+++ b/crates/formality-prove/src/prove/minimize/test.rs
@@ -23,7 +23,7 @@ fn minimize_a() {
     let (mut env_min, term_min, m) = minimize(env, term);
 
     expect!["(Env { variables: [?ty_0, ?ty_1], coherence_mode: false }, [?ty_0, ?ty_1])"]
-    .assert_eq(&format!("{:?}", (&env_min, &term_min)));
+        .assert_eq(&format!("{:?}", (&env_min, &term_min)));
 
     let ty0 = term_min[0].as_variable().unwrap();
     let ty1 = term_min[1].as_variable().unwrap();
diff --git a/examples/formality-eg/type_system.rs b/examples/formality-eg/type_system.rs
index e69de29b..8b137891 100644
--- a/examples/formality-eg/type_system.rs
+++ b/examples/formality-eg/type_system.rs
@@ -0,0 +1 @@
+

From c9534a00dd139aecc37f6ceef54b5bc2cadf6a26 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 11 Nov 2023 06:15:26 -0500
Subject: [PATCH 04/11] elide defaulted fields in debug output

---
 crates/formality-macros/src/debug.rs | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/crates/formality-macros/src/debug.rs b/crates/formality-macros/src/debug.rs
index 98401013..69c1a206 100644
--- a/crates/formality-macros/src/debug.rs
+++ b/crates/formality-macros/src/debug.rs
@@ -242,7 +242,7 @@ fn debug_variant_with_attr(
 
 fn debug_field_with_mode(name: &Ident, mode: &FieldMode) -> TokenStream {
     match mode {
-        FieldMode::Single | FieldMode::Optional => {
+        FieldMode::Single => {
             quote_spanned! { name.span() =>
                 write!(fmt, "{}", sep)?;
                 write!(fmt, "{:?}", #name)?;
@@ -250,6 +250,16 @@ fn debug_field_with_mode(name: &Ident, mode: &FieldMode) -> TokenStream {
             }
         }
 
+        FieldMode::Optional => {
+            quote_spanned! { name.span() =>
+                if !::formality_core::util::is_default(#name) {
+                    write!(fmt, "{}", sep)?;
+                    write!(fmt, "{:?}", #name)?;
+                    sep = " ";
+                }
+            }
+        }
+
         FieldMode::Many => {
             quote_spanned! { name.span() =>
                 for e in #name {

From 0e5464cd3fe458fff31eb29be3cc95b21a9b6d89 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 11:35:57 +0000
Subject: [PATCH 05/11] pretty-print `Safety`

---
 crates/formality-prove/src/decls.rs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs
index 25e7aa64..ed94f45c 100644
--- a/crates/formality-prove/src/decls.rs
+++ b/crates/formality-prove/src/decls.rs
@@ -1,3 +1,5 @@
+use std::fmt;
+
 use formality_core::{set, Set, Upcast};
 use formality_macros::term;
 use formality_types::grammar::{
@@ -141,6 +143,7 @@ pub struct NegImplDeclBoundData {
 }
 
 #[term]
+#[customize(debug)]
 #[derive(Default)]
 pub enum Safety {
     #[default]
@@ -148,6 +151,15 @@ pub enum Safety {
     Unsafe,
 }
 
+impl fmt::Debug for Safety {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Safety::Safe => write!(f, "safe"),
+            Safety::Unsafe => write!(f, "unsafe"),
+        }
+    }
+}
+
 /// A "trait declaration" declares a trait that exists, its generics, and its where-clauses.
 /// It doesn't capture the trait items, which will be transformed into other sorts of rules.
 ///

From 866b4da762c8187406623aa0b006cf7d5831a31a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 12:23:55 +0000
Subject: [PATCH 06/11] match trait safety errors from rustc

---
 crates/formality-check/src/impls.rs | 27 +++++++++++++--------------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
index 43fe28e1..ab61622a 100644
--- a/crates/formality-check/src/impls.rs
+++ b/crates/formality-check/src/impls.rs
@@ -6,8 +6,8 @@ use formality_prove::{Env, Safety};
 use formality_rust::{
     grammar::{
         AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, AssociatedTyValueBoundData, Fn,
-        FnBoundData, ImplItem, NegTraitImpl, NegTraitImplBoundData, TraitBoundData, TraitImpl,
-        TraitImplBoundData, TraitItem,
+        FnBoundData, ImplItem, NegTraitImpl, NegTraitImplBoundData, Trait, TraitBoundData,
+        TraitImpl, TraitImplBoundData, TraitItem,
     },
     prove::ToWcs,
 };
@@ -45,7 +45,7 @@ impl super::Check<'_> {
             trait_items,
         } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?;
 
-        self.check_safety_matches(&trait_decl.safety, safety)?;
+        self.check_safety_matches(&trait_decl, safety)?;
 
         for impl_item in &impl_items {
             self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?;
@@ -73,17 +73,16 @@ impl super::Check<'_> {
         Ok(())
     }
 
-    /// Validate `unsafe trait` and `unsafe impl` line up
-    fn check_safety_matches(&self, trait_decl: &Safety, trait_impl: &Safety) -> Fallible<()> {
-        match trait_decl {
-            Safety::Safe => anyhow::ensure!(
-                matches!(trait_impl, Safety::Safe),
-                "implementing the trait is not `unsafe`"
-            ),
-            Safety::Unsafe => anyhow::ensure!(
-                matches!(trait_impl, Safety::Unsafe),
-                "the trait requires an `unsafe impl` declaration"
-            ),
+    /// Validate that the declared safety of an impl matches the one from the trait declaration.
+    fn check_safety_matches(&self, trait_decl: &Trait, trait_impl: &Safety) -> Fallible<()> {
+        if trait_decl.safety != *trait_impl {
+            match trait_decl.safety {
+                Safety::Safe => bail!("implementing the trait `{:?}` is not unsafe", trait_decl.id),
+                Safety::Unsafe => bail!(
+                    "the trait `{:?}` requires an `unsafe impl` declaration",
+                    trait_decl.id
+                ),
+            }
         }
         Ok(())
     }

From f562ada7e29163ca7de321c6b13624d1ce7ba52b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 12:25:55 +0000
Subject: [PATCH 07/11] add decl safety tests

---
 "tests/ui/decl_safety/safe_trait.\360\237\224\254"         | 7 +++++++
 tests/ui/decl_safety/safe_trait_mismatch.stderr            | 4 ++++
 .../ui/decl_safety/safe_trait_mismatch.\360\237\224\254"   | 6 ++++++
 "tests/ui/decl_safety/unsafe_trait.\360\237\224\254"       | 7 +++++++
 tests/ui/decl_safety/unsafe_trait_mismatch.stderr          | 4 ++++
 .../ui/decl_safety/unsafe_trait_mismatch.\360\237\224\254" | 6 ++++++
 6 files changed, 34 insertions(+)
 create mode 100644 "tests/ui/decl_safety/safe_trait.\360\237\224\254"
 create mode 100644 tests/ui/decl_safety/safe_trait_mismatch.stderr
 create mode 100644 "tests/ui/decl_safety/safe_trait_mismatch.\360\237\224\254"
 create mode 100644 "tests/ui/decl_safety/unsafe_trait.\360\237\224\254"
 create mode 100644 tests/ui/decl_safety/unsafe_trait_mismatch.stderr
 create mode 100644 "tests/ui/decl_safety/unsafe_trait_mismatch.\360\237\224\254"

diff --git "a/tests/ui/decl_safety/safe_trait.\360\237\224\254" "b/tests/ui/decl_safety/safe_trait.\360\237\224\254"
new file mode 100644
index 00000000..dd6610a4
--- /dev/null
+++ "b/tests/ui/decl_safety/safe_trait.\360\237\224\254"
@@ -0,0 +1,7 @@
+//@check-pass
+[
+    crate baguette {
+        safe trait Foo {}
+        safe impl Foo for u32 {}
+    }
+]
diff --git a/tests/ui/decl_safety/safe_trait_mismatch.stderr b/tests/ui/decl_safety/safe_trait_mismatch.stderr
new file mode 100644
index 00000000..374a2982
--- /dev/null
+++ b/tests/ui/decl_safety/safe_trait_mismatch.stderr
@@ -0,0 +1,4 @@
+Error: check_trait_impl(unsafe impl Foo for u32 { })
+
+Caused by:
+    implementing the trait `Foo` is not unsafe
diff --git "a/tests/ui/decl_safety/safe_trait_mismatch.\360\237\224\254" "b/tests/ui/decl_safety/safe_trait_mismatch.\360\237\224\254"
new file mode 100644
index 00000000..7a2f8d41
--- /dev/null
+++ "b/tests/ui/decl_safety/safe_trait_mismatch.\360\237\224\254"
@@ -0,0 +1,6 @@
+[
+    crate baguette {
+        trait Foo {}
+        unsafe impl Foo for u32 {}
+    }
+]
diff --git "a/tests/ui/decl_safety/unsafe_trait.\360\237\224\254" "b/tests/ui/decl_safety/unsafe_trait.\360\237\224\254"
new file mode 100644
index 00000000..f93b0dac
--- /dev/null
+++ "b/tests/ui/decl_safety/unsafe_trait.\360\237\224\254"
@@ -0,0 +1,7 @@
+//@check-pass
+[
+    crate baguette {
+        unsafe trait Foo {}
+        unsafe impl Foo for u32 {}
+    }
+]
diff --git a/tests/ui/decl_safety/unsafe_trait_mismatch.stderr b/tests/ui/decl_safety/unsafe_trait_mismatch.stderr
new file mode 100644
index 00000000..662e2398
--- /dev/null
+++ b/tests/ui/decl_safety/unsafe_trait_mismatch.stderr
@@ -0,0 +1,4 @@
+Error: check_trait_impl(impl Foo for u32 { })
+
+Caused by:
+    the trait `Foo` requires an `unsafe impl` declaration
diff --git "a/tests/ui/decl_safety/unsafe_trait_mismatch.\360\237\224\254" "b/tests/ui/decl_safety/unsafe_trait_mismatch.\360\237\224\254"
new file mode 100644
index 00000000..48c1b0cd
--- /dev/null
+++ "b/tests/ui/decl_safety/unsafe_trait_mismatch.\360\237\224\254"
@@ -0,0 +1,6 @@
+[
+    crate baguette {
+        unsafe trait Foo {}
+        impl Foo for u32 {}
+    }
+]

From 72062fce145be124af15838dd4daab1d30c172f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 12:38:17 +0000
Subject: [PATCH 08/11] slight `check_trait_impl` cleanup

---
 crates/formality-check/src/impls.rs | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
index ab61622a..d7d92d41 100644
--- a/crates/formality-check/src/impls.rs
+++ b/crates/formality-check/src/impls.rs
@@ -17,10 +17,8 @@ use formality_types::{
 };
 
 impl super::Check<'_> {
-    #[context("check_trait_impl({v:?})")]
-    pub(super) fn check_trait_impl(&self, v: &TraitImpl) -> Fallible<()> {
-        let TraitImpl { binder, safety } = v;
-
+    #[context("check_trait_impl({trait_impl:?})")]
+    pub(super) fn check_trait_impl(&self, trait_impl: &TraitImpl) -> Fallible<()> {
         let mut env = Env::default();
 
         let TraitImplBoundData {
@@ -29,7 +27,7 @@ impl super::Check<'_> {
             trait_parameters,
             where_clauses,
             impl_items,
-        } = env.instantiate_universally(binder);
+        } = env.instantiate_universally(&trait_impl.binder);
 
         let trait_ref = trait_id.with(self_ty, trait_parameters);
 
@@ -45,7 +43,7 @@ impl super::Check<'_> {
             trait_items,
         } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?;
 
-        self.check_safety_matches(&trait_decl, safety)?;
+        self.check_safety_matches(&trait_decl, &trait_impl)?;
 
         for impl_item in &impl_items {
             self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item)?;
@@ -74,8 +72,8 @@ impl super::Check<'_> {
     }
 
     /// Validate that the declared safety of an impl matches the one from the trait declaration.
-    fn check_safety_matches(&self, trait_decl: &Trait, trait_impl: &Safety) -> Fallible<()> {
-        if trait_decl.safety != *trait_impl {
+    fn check_safety_matches(&self, trait_decl: &Trait, trait_impl: &TraitImpl) -> Fallible<()> {
+        if trait_decl.safety != trait_impl.safety {
             match trait_decl.safety {
                 Safety::Safe => bail!("implementing the trait `{:?}` is not unsafe", trait_decl.id),
                 Safety::Unsafe => bail!(

From e03258c4b895c901c2ecdf8967e2947b2e999811 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 12:48:57 +0000
Subject: [PATCH 09/11] implement safety check for negative impls

---
 crates/formality-check/src/impls.rs | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
index d7d92d41..b7b9b491 100644
--- a/crates/formality-check/src/impls.rs
+++ b/crates/formality-check/src/impls.rs
@@ -52,7 +52,8 @@ 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 {
@@ -60,10 +61,15 @@ impl super::Check<'_> {
             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())?;

From 4d615b163a17e6c47b02e15ee0c434ae6f043a22 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 12:49:22 +0000
Subject: [PATCH 10/11] add tests for safe/unsafe negative impls

---
 .../decl_safety/safe_trait-negative_impl_mismatch.stderr   | 4 ++++
 .../safe_trait-negative_impl_mismatch.\360\237\224\254"    | 6 ++++++
 .../unsafe_trait-negative_impl.\360\237\224\254"           | 7 +++++++
 .../decl_safety/unsafe_trait-negative_impl_mismatch.stderr | 4 ++++
 .../unsafe_trait-negative_impl_mismatch.\360\237\224\254"  | 6 ++++++
 5 files changed, 27 insertions(+)
 create mode 100644 tests/ui/decl_safety/safe_trait-negative_impl_mismatch.stderr
 create mode 100644 "tests/ui/decl_safety/safe_trait-negative_impl_mismatch.\360\237\224\254"
 create mode 100644 "tests/ui/decl_safety/unsafe_trait-negative_impl.\360\237\224\254"
 create mode 100644 tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.stderr
 create mode 100644 "tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.\360\237\224\254"

diff --git a/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.stderr b/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.stderr
new file mode 100644
index 00000000..00127498
--- /dev/null
+++ b/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.stderr
@@ -0,0 +1,4 @@
+Error: check_neg_trait_impl(unsafe impl ! Foo for u32 {})
+
+Caused by:
+    negative impls cannot be unsafe
diff --git "a/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.\360\237\224\254" "b/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.\360\237\224\254"
new file mode 100644
index 00000000..cad4149a
--- /dev/null
+++ "b/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.\360\237\224\254"
@@ -0,0 +1,6 @@
+[
+    crate baguette {
+        trait Foo {}
+        unsafe impl !Foo for u32 {}
+    }
+]
diff --git "a/tests/ui/decl_safety/unsafe_trait-negative_impl.\360\237\224\254" "b/tests/ui/decl_safety/unsafe_trait-negative_impl.\360\237\224\254"
new file mode 100644
index 00000000..a1fdf102
--- /dev/null
+++ "b/tests/ui/decl_safety/unsafe_trait-negative_impl.\360\237\224\254"
@@ -0,0 +1,7 @@
+//@check-pass
+[
+    crate baguette {
+        unsafe trait Foo {}
+        impl !Foo for u32 {}
+    }
+]
diff --git a/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.stderr b/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.stderr
new file mode 100644
index 00000000..00127498
--- /dev/null
+++ b/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.stderr
@@ -0,0 +1,4 @@
+Error: check_neg_trait_impl(unsafe impl ! Foo for u32 {})
+
+Caused by:
+    negative impls cannot be unsafe
diff --git "a/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.\360\237\224\254" "b/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.\360\237\224\254"
new file mode 100644
index 00000000..2ba98a14
--- /dev/null
+++ "b/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.\360\237\224\254"
@@ -0,0 +1,6 @@
+[
+    crate baguette {
+        unsafe trait Foo {}
+        unsafe impl !Foo for u32 {}
+    }
+]

From 53d0e43a51f98a572d69b3373c55c54413e49bb7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Rakic?= <remy.rakic+github@gmail.com>
Date: Sat, 11 Nov 2023 13:00:44 +0000
Subject: [PATCH 11/11] add documentation to `Safety`

---
 crates/formality-prove/src/decls.rs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs
index ed94f45c..6f725c01 100644
--- a/crates/formality-prove/src/decls.rs
+++ b/crates/formality-prove/src/decls.rs
@@ -142,6 +142,7 @@ pub struct NegImplDeclBoundData {
     pub where_clause: Wcs,
 }
 
+/// Mark a trait or trait impl as `unsafe`.
 #[term]
 #[customize(debug)]
 #[derive(Default)]