`deriving` does not handle `unsafe` (or `noncomputable`)

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The deriving mechanism does not copy across unsafe attributes, and so cannot be used in the presence of unsafe code.

Perhaps erroring here is deliberate to avoid accidental creation of unsafe code; in which case, deriving unsafe Repr, unsafe BEq might be an acceptable solution.

Note that the same problem also occurs for noncomputable, though that can be handled with noncomputable section

Context

Zulip message

Steps to Reproduce

1. Run the following

   structure Foo
   
   unsafe instance : Repr Foo where
     reprPrec f n := "foo"
   
   unsafe instance : BEq Foo where
     beq f₁ f₂ := true
   
   structure Bar where
     foo : Foo
   deriving Repr, BEq
   

Expected behavior: unsafe instance : BEq Bar and unsafe instance : Repr Bar are created

Actual behavior: (kernel) invalid declaration, it uses unsafe declaration 'instReprFoo'

Versions

4.6.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal self-contained Lean reproduction from the issue on version 4.6.0-rc1, then trace the deriving mechanism that processes Repr and BEq instances. Done means the derived instances for Bar are created with the required unsafe status without the invalid-declaration error, with the analogous noncomputable behavior understood as well.