Kernel accepts wrong-structure projections, allowing an axiom-free proof of False

Prerequisites

Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues
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, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)

Description

Lean accepts a checked declaration containing a projection whose structure name does not match the value being projected.

The repro below uses the ordinary checked addDecl path. It then proves False with no axioms. It does not use sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file.

Context

Found while reviewing a proof by @xrchz of the Collatz Conjecture in less than 300 lines:

https://github.com/xrchz/CollatzLean/blob/a79357462a33d2a6babd4cf6c8d8bcd25425d653/Collatz/Main.lean

I found related projection and soundness reports, but this appears to be distinct.

Steps to Reproduce

Save this file as Bug.lean.

import Lean
open Lean Elab Command

inductive P : Prop where | mk (b : Bool)
structure C where b : Bool
inductive W : Type where | mk (p : P)
inductive L (α : Type) (b : Bool) : Type where | mk
inductive T : Bool → Prop where | mk : T true

def pad (e : Expr) (n : Nat) : Expr :=
  mkApp (mkLambda `x .default (mkConst ``Nat) e) (.lit (.natVal n))

meta def build : CommandElabM Unit := do
  let f := pad (mkConst ``Bool.false) 78670
  let t := pad (mkConst ``Bool.true) 24083
  unless f.hash == t.hash && f.approxDepth == t.approxDepth do
    throwError "hash collision failed"
  let fw := mkApp (mkConst ``W.mk) (mkApp (mkConst ``P.mk) f)
  let tw := mkApp (mkConst ``W.mk) (mkApp (mkConst ``P.mk) t)
  let w := mkBVar 0
  let Ew := mkApp (mkConst `E) w
  let b := mkProj ``C 0 (mkProj ``C 0 w)
  let l := mkApp2 (mkConst ``L) Ew b
  let Et := mkForall `w .default (mkConst ``W) (mkSort 1)
  let ct := mkForall `w .default (mkConst ``W) <|
    mkForall `l .default l (mkApp (mkConst `E) (mkBVar 1))
  liftCoreM <| addDecl <| .inductDecl [] 1 [{
    name := `E, type := Et, ctors := [{ name := `E.mk, type := ct }] }] false
  let Et := mkApp (mkConst `E) tw
  let l := mkApp2 (mkConst ``L.mk) Et (mkConst ``Bool.true)
  liftCoreM <| addDecl <| .defnDecl {
    name := `e, levelParams := [], type := Et,
    value := mkApp2 (mkConst `E.mk) tw l,
    hints := .abbrev, safety := .safe }
  liftCoreM <| addDecl <| .defnDecl {
    name := `good', levelParams := [],
    type := mkApp (mkConst ``T) t, value := mkConst ``T.mk,
    hints := .abbrev, safety := .safe }
  let Ef := mkApp (mkConst `E) fw
  let Et := mkApp (mkConst `E) tw
  let a := mkApp2 (mkConst `E.mk) fw (mkProj `E 0 (mkConst `e))
  let tl := mkApp2 (mkConst ``L.mk) Et (mkConst ``Bool.true)
  let b := mkApp2 (mkConst `E.mk) tw tl
  let cT := mkApp2 (mkConst ``L) Et t
  let c := mkApp (mkLambda `l .default cT (mkConst ``Unit.unit)) tl
  let fl := mkApp2 (mkConst ``L.mk) Ef f
  let d := mkApp2 (mkConst `E.mk) fw fl
  let v := Expr.letE `a Ef a
    (.letE `b Et b
      (.letE `c (mkConst ``Unit) c
        (.letE `d Ef d (mkConst `good') true) true) true) true
  liftCoreM <| addDecl <| .thmDecl {
    name := `bad, levelParams := [],
    type := mkApp (mkConst ``T) f, value := v }

elab "mkbug" : command => build
mkbug
theorem boom : False := nomatch (bad : T false)
#print axioms bad
#print axioms boom

Run:

Lean accepts the file.

Expected behavior: Lean should reject the declaration of E, because its constructor type contains C projections applied to a W.

Actual behavior: Lean accepts the file and prints:

'bad' does not depend on any axioms
'boom' does not depend on any axioms

Versions

Lean (version 4.34.0-nightly-2026-07-27, arm64-apple-darwin24.6.0, commit 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402, Release)

OS:

Impact

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

The issue affects checked-kernel soundness. An adversarial metaprogram can add declarations that ordinary Lean code then uses to prove False, with #print axioms reporting no axioms.