Compiler PANIC in `ExplicitBoxing` when `deriving Repr`/`BEq` over an `unsafe instance`

Prerequisites

• Check that your issue is not already filed
• Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release

Description

Deriving Repr or BEq for a structure whose field type only has an unsafe instance panics the compiler. The kernel correctly rejects the derived instance, but compilation proceeds anyway and hits unreachable! in the ExplicitBoxing LCNF pass, emitting five chained PANIC messages.

Writing the same instance by hand produces a clean kernel error and no panic, so the panic is specific to the deriving path.

Context

Noticed while checking whether #3498 (deriving does not handle unsafe or noncomputable) still reproduces. The underlying "cannot derive over unsafe" behaviour is #3498; this issue is only about the panic.

This looks like the unsafe counterpart of a panic already fixed for noncomputable: same pass and same unreachable! as #13371 and #13921, whose deriving-related flavour was fixed in #14125. That fix was in Deriving/Inhabited.lean's aux-function path; this case goes through processDefDeriving/mkDefinitionValInferringUnsafe in Deriving/Basic.lean, so it is not covered by it.

Steps to Reproduce

structure Foo

unsafe instance : Repr Foo where
  reprPrec f n := "foo"

structure Bar where
  foo : Foo
deriving Repr

Expected behavior: an error explaining that the instance cannot be derived because it depends on an unsafe declaration — as happens when the instance is written by hand.

Actual behavior:

error: (kernel) invalid declaration, it uses unsafe declaration 'instReprFoo'
error: failed to compile definition, compiler IR check failed at `instReprBar._closed_0`.
       Error: unknown join point 'block_0'
PANIC at ...ExplicitBoxing.tryCorrectLetDeclType Lean.Compiler.LCNF.ExplicitBoxing:301:45: unreachable code has been reached
PANIC at ...ExplicitBoxing.visitLet Lean.Compiler.LCNF.ExplicitBoxing:336:45: unreachable code has been reached
PANIC at Std.DTreeMap.Internal.Impl.Const.get! Std.Data.DTreeMap.Internal.Queries:227:13: Key is not present in map
PANIC at Option.get! Init.Data.Option.BasicAux:22:14: value is none
PANIC at Std.DHashMap.Internal.AssocList.get! Std.Data.DHashMap.Internal.AssocList.Basic:163:11: key is not present in hash table

Versions

Reproduces on both:

• Lean 4.35.0-nightly-2026-09-04, arm64-apple-darwin24.6.0 macOS
• Lean 4.33.1 (stable), arm64-apple-darwin24.6.0 macOS

macOS 26.5.2, arm64.

Additional Information

deriving BEq panics identically (instBEqBar._closed_0).

The panics cascade across three passes: ExplicitBoxing.tryCorrectLetDeclType → visitLet, then
LCNF.Decl.explicitRc, then Lean.IR.ToIR.getJoinPointValue inside lowerCode — the last of which
is where the unknown join point 'block_0' IR check error originates.

Deriving over an unsafe inductive does not panic — it gives a clean
(kernel) invalid declaration, it uses unsafe declaration 'Foo':

unsafe inductive Foo where
  | default : Foo
  | io : IO Foo → Foo
  deriving Inhabited

The same instance written by hand errors cleanly, with no panic:

structure Foo
unsafe instance : Repr Foo where
  reprPrec f n := "foo"
structure Bar where
  foo : Foo
instance : Repr Bar where
  reprPrec b n := reprPrec b.foo n

Investigation of this issue was assisted by Claude; the repros were run and checked manually.

Impact

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

Start with the minimal Repr and BEq reproductions and trace the deriving path through Deriving/Basic.lean, especially processDefDeriving and mkDefinitionValInferringUnsafe, into ExplicitBoxing.tryCorrectLetDeclType and visitLet. Compare the behavior with the existing noncomputable fix in Deriving/Inhabited.lean; done means a clean kernel error for unsafe-derived instances without compiler PANIC messages.