Improvements to unsafe trait support

crates/formality-check/src/impls.rs

@@ -19,6 +19,8 @@ use formality_types::{
 impl super::Check<'_> {
     #[context("check_trait_impl({trait_impl:?})")]
     pub(super) fn check_trait_impl(&self, trait_impl: &TraitImpl) -> Fallible<()> {
+        let TraitImpl { binder, safety: _ } = trait_impl;
+
         let mut env = Env::default();
 
         let TraitImplBoundData {
@@ -27,7 +29,7 @@ impl super::Check<'_> {
             trait_parameters,
             where_clauses,
             impl_items,
-        } = env.instantiate_universally(&trait_impl.binder);
+        } = env.instantiate_universally(&binder);
 
         let trait_ref = trait_id.with(self_ty, trait_parameters);
 
@@ -54,19 +56,21 @@ impl super::Check<'_> {
 
     #[context("check_neg_trait_impl({trait_impl:?})")]
     pub(super) fn check_neg_trait_impl(&self, trait_impl: &NegTraitImpl) -> Fallible<()> {
+        let NegTraitImpl { binder, safety } = trait_impl;
+
         let mut env = Env::default();
 
         let NegTraitImplBoundData {
             trait_id,
             self_ty,
             trait_parameters,
             where_clauses,
-        } = env.instantiate_universally(&trait_impl.binder);
+        } = env.instantiate_universally(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 {
+        if *safety == Safety::Unsafe {
             bail!("negative impls cannot be unsafe");
         }
 

crates/formality-prove/src/decls.rs

@@ -1,5 +1,3 @@
-use std::fmt;
-
 use formality_core::{set, Set, Upcast};
 use formality_macros::term;
 use formality_types::grammar::{
@@ -144,23 +142,13 @@ pub struct NegImplDeclBoundData {
 
 /// Mark a trait or trait impl as `unsafe`.
 #[term]
-#[customize(debug)]
 #[derive(Default)]
 pub enum Safety {
     #[default]
     Safe,
     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.
 ///