Miscompilation (incorrect code) in new compiler

Stream: lean4

[George Pîrlea]

I've encountered a miscompilation issue in the new compiler (all versions since v4.22.0 up to and including v4.24.0-rc1, as well as 4.25.0-nightly-2025-09-17 manifest it). Basically, the behaviour of a function (Module.getStateBinders) depends on whether a distinct but similar function (Module.getTheoryBinders) has been compiled. I suspect there's some code reuse optimisation going badly wrong.

Is this a known issue? If not, I can report it on GitHub. (I couldn't find anything on the issue tracker, but maybe I missed it.)

Apologies for not being able to minimise this further — it was extracted from a fairly large development. Here's the file: Miscompilation.lean

import Lean
open Lean Parser

namespace Veil

inductive Mutability where
  | mutable
  | immutable
  | inherit
deriving Inhabited, BEq, Hashable, Repr

inductive StateComponentType where
  | simple (t : TSyntax ``Command.structSimpleBinder)
  | complex (binders : TSyntaxArray ``Term.bracketedBinder) (dom : Term)
deriving Inhabited, BEq

structure StateComponent where
  mutability : Mutability
  name       : Name
  type       : StateComponentType
deriving Inhabited, BEq

structure Module where
  name : Name
  signature : Array StateComponent
deriving Inhabited

end Veil

section Util
set_option autoImplicit true
def getSimpleBinderType [Monad m] [MonadError m] (sig : TSyntax `Lean.Parser.Command.structSimpleBinder) : m (TSyntax `term) := do
  match sig with
  | `(Lean.Parser.Command.structSimpleBinder| $_:ident : $tp:term) => pure tp
  | _ => throwError s!"getSimpleBinderType: don't know how to handle {sig}"

def mkArrowStx [Monad m] [MonadQuotation m] [MonadError m] (tps : List Term) (terminator : Option $ TSyntax `term := none) : m (TSyntax `term) := do
  match tps with
  | [] => if let some t := terminator then return t else throwError "empty list of types and no terminator"
  | [a] => match terminator with
    | none => `(term| $a)
    | some t => `(term| $a -> $t)
  | a :: as =>
    let cont ← mkArrowStx as terminator
    `(term| $a -> $cont)

def complexBinderToSimpleBinder [Monad m] [MonadQuotation m] [MonadError m] (nm : TSyntax `ident) (br : TSyntaxArray `Lean.Parser.Term.bracketedBinder) (domT : TSyntax `term) : m (TSyntax `Lean.Parser.Command.structSimpleBinder) := do
  let types ← br.mapM fun m => match m with
    | `(bracketedBinder| ($_arg:ident : $tp:term)) => return tp
    | _ => throwError "Invalid binder syntax {br}"
  let typeStx ← mkArrowStx types.toList domT
  let simple ← `(Lean.Parser.Command.structSimpleBinder| $nm:ident : $typeStx)
  return simple
end Util

open Lean Parser Elab Command Term

namespace Veil

instance : ToString Mutability where
  toString
    | Mutability.mutable => "mutable"
    | Mutability.immutable => "immutable"
    | Mutability.inherit => "inherit"

instance : ToString StateComponentType where
  toString
    | StateComponentType.simple t => toString t
    | StateComponentType.complex b d  => s!"{b} : {d}"

instance : ToString StateComponent where
  toString sc := s!"{sc.mutability} {sc.name} {sc.type}"

def StateComponentType.stx [Monad m] [MonadQuotation m] [MonadError m] (sct : StateComponentType) : m (TSyntax `term) := do
  match sct with
  | .simple t => getSimpleBinderType t
  | .complex b d => getSimpleBinderType $ ← complexBinderToSimpleBinder (mkIdent Name.anonymous) b d

/-- Returns, e.g., `initial_msg : address → address → round → value → Prop` -/
def StateComponent.getSimpleBinder [Monad m] [MonadQuotation m] [MonadError m] (sc : StateComponent) : m (TSyntax ``Command.structSimpleBinder) := do
  match sc.type with
  | .simple t => return t
  | .complex b d => return ← complexBinderToSimpleBinder (mkIdent sc.name) b d

def StateComponent.stx {m} [Monad m] [MonadQuotation m] [MonadError m] (sc : StateComponent) : m Syntax := sc.getSimpleBinder
def StateComponent.typeStx [Monad m] [MonadQuotation m] [MonadError m] (sc : StateComponent) : m Term := sc.type.stx

def Module.getTheoryBinders [Monad m] [MonadQuotation m] [MonadError m] (mod : Module) : m (Array (TSyntax `Lean.Parser.Term.bracketedBinder)) := do
  mod.signature.filterMapM fun sc => do
    match sc.mutability with
    | .immutable => return .some $ ← `(bracketedBinder| ($(mkIdent sc.name) : $(← sc.typeStx)))
    | _ => pure .none

def Module.getStateBinders [Monad m] [MonadQuotation m] [MonadError m] (mod : Module) : m (Array (TSyntax `Lean.Parser.Term.bracketedBinder)) := do
  dbg_trace "[INPUT] {mod.signature}"
  let res ← mod.signature.filterMapM fun sc => do
    match sc.mutability with
    | .mutable =>
    -- dbg_trace "getStateBinders -> {sc.name} is mutable"
    return .some $ ← `(bracketedBinder| ($(mkIdent sc.name) : $(← sc.typeStx)))
    | _ =>
    -- NOTE 1: uncommenting this line makes `trigger` work correctly
    -- dbg_trace "getStateBinders -> {sc.name} is not mutable"
    pure .none
  dbg_trace "[RESULT] {res}"
  return res

-- NOTE 2: commenting out this function (or the `trace` statement) makes `trigger` work correctly
def interference (mod : Module) : CommandElabM Unit := do
  trace[veil.debug] "theory binders: {← mod.getTheoryBinders}"
  return

end Veil

namespace Veil

open Lean Parser Elab Command
def trigger : CommandElabM Unit := do
  let sig : Array StateComponent := #[
    { mutability := .mutable, name := `leader, «type» := .simple $ ← `(Command.structSimpleBinder| x : Nat → Bool)},
    { mutability := .mutable, name := `pending, «type» := .simple $ ← `(Command.structSimpleBinder| pending : Nat → Nat → Bool)}
  ]
  let emptyMod : Module := default
  let mod := { emptyMod with signature := sig}
  trace[debug] "stateBinders: {← mod.getStateBinders}"
  return ()

set_option trace.debug true
#eval trigger
-- incorrect result: `[RESULT] #[]`
-- correct result: (something other than `#[]` gets printed), i.e.

/-
Either of the following actions seem to "fix" the issue:
  - removing the `inherit` constructor from the `Mutability` enum (and from the `ToString Mutability` instance)
  - uncommenting one of the `dbg_trace` statements in `getStateBinders`
  - commenting out the `interference` function (or just the `trace` statement within it)

My (uninformed) guess is somehow the closure passed to `filterMapM` in
`getTheoryBinders` gets confused/conflated with the one in `getStateBinders`.
-/

#version
-- This manifests with:
-- Lean 4.25.0-nightly-2025-09-17 / Target: x86_64-unknown-linux-gnu
-- Lean 4.24.0-rc1 / Target: arm64-apple-darwin23.6.0 macOS
-- Lean 4.23.0 / Target: arm64-apple-darwin23.6.0 macOS
-- Lean 4.22.0 / Target: arm64-apple-darwin23.6.0 macOS
-- Does NOT manifest with:
-- Lean 4.21.0 / Target: arm64-apple-darwin23.6.0 macOS

end Veil

[Sebastian Ullrich]

Thank you for the comprehensive report, this is indeed an incorrect reuse of a specialization result. We are looking into it.

[Henrik Böving]

fixed in lean4#10429 @George Pîrlea

[George Pîrlea]

Thank you very much for the quick fix!

[George Pîrlea]

@Sebastian Ullrich @Henrik Böving Would it be possible to push this into an v4.24.0 RC release?

[George Pîrlea]

For context: I worked around the specific instance I reported, but I keep running into strange behaviour that I suspect is due to the same issue. It seems quite easy to trigger.

[Kim Morrison]

@George Pîrlea, I'm happy to put this on the releases/v4.24.0 branch, which means that if we cut a new release candidate it will arrive there, and it will end up in the stable release v4.24.0, but it's substantial work for make a new release candidate. Can you just live on the nightly toolchains in the meantime?

[George Pîrlea]

I can wait for the next RC. Thank you!

I'm not on nightly, since we indirectly depend on mathlib, but I can keep working around the issue when I encounter it (by adding dbg_trace to my code). It's annoying, but not a show-stopper.