Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

bug: `isExclusiveUnsafe` should be marked `@[never_extract]`

Open Beginner friendly
  • Is something wrong?
#15,925 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
1/5
Estimated time
Under an hour
Newbie friendliness
85/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
compilers
Domain
compilers

Research direction

Open Init/Util.lean and locate the unsafe opaque declarations isExclusiveUnsafe and ptrAddrUnsafe. Add the @[never_extract] attribute before each, as proposed. Rebuild Lean with lake build and run the reproduction from the issue to confirm the second exclusivity check returns false after sharing the reference.

Written by the indexing model from the issue text.

Description

bug
Description

isExclusiveUnsafe (Init/Util.lean) is declared as @[extern "lean_is_exclusive_obj"] unsafe opaque isExclusiveUnsafe {α} (a : @& α) : Bool, without @[never_extract], so the compiler treats it as pure. Common subexpression elimination then merges two checks of the same variable even when the variable is shared between them. The second check reports true (exclusive) for an object whose reference count is 2. Code that writes in place based on that answer, which is what this primitive exists for, would mutate an object that is still visible through another reference.

Calls on closed terms are also extracted into _closed constants. On current toolchains the extracted value is false, because the closed argument is made persistent first, so I have not seen that case give a wrong answer. Still, the check is then evaluated only once, which is not what the primitive means. ptrAddrUnsafe is missing the same attribute and is extracted the same way.

Context

This came up while writing in-place update code for unboxed scalar arrays that branches on isExclusiveUnsafe.

Steps to Reproduce

lakefile.toml: name = "repro", one [[lean_exe]] with name = "repro" and root = "Main".

Main.lean:

@[never_extract, extern "lean_is_exclusive_obj"]
unsafe opaque myIsExclusive {α : Type u} (a : @& α) : Bool

/-- Check `a`, share it by storing it in a ref, then check again. -/
@[noinline] unsafe def coreImpl (a : Array Nat) : IO (Bool × Bool × Array Nat) := do
  let e1 := isExclusiveUnsafe a
  let r ← IO.mkRef a
  let e2 := isExclusiveUnsafe a
  return (e1, e2, (← r.get) ++ a)

@[noinline] unsafe def mineImpl (a : Array Nat) : IO (Bool × Bool × Array Nat) := do
  let e1 := myIsExclusive a
  let r ← IO.mkRef a
  let e2 := myIsExclusive a
  return (e1, e2, (← r.get) ++ a)

@[implemented_by coreImpl] opaque core : Array Nat → IO (Bool × Bool × Array Nat)
@[implemented_by mineImpl] opaque mine : Array Nat → IO (Bool × Bool × Array Nat)

-- closed-term extraction through an inlined helper
@[inline] unsafe def isExclInl (a : Array Nat) : Bool := isExclusiveUnsafe a
@[inline] unsafe def myIsExclInl (a : Array Nat) : Bool := myIsExclusive a
unsafe def closedCoreImpl (n : Nat) : Bool := n == 0 && isExclInl #[1, 2, 3]
unsafe def closedMineImpl (n : Nat) : Bool := n == 0 && myIsExclInl #[1, 2, 3]
@[implemented_by closedCoreImpl] opaque closedCore : Nat → Bool
@[implemented_by closedMineImpl] opaque closedMine : Nat → Bool

@[noinline] def fresh (n : Nat) : Array Nat := Array.replicate 3 n

def main (args : List String) : IO Unit := do
  let n := args.length
  let (c1, c2, _) ← core (fresh n)
  let (m1, m2, _) ← mine (fresh (n + 1))
  IO.println s!"isExclusiveUnsafe: before share = {c1}, after share = {c2}"
  IO.println s!"never_extract    : before share = {m1}, after share = {m2}"
  IO.println s!"closed: core = {closedCore n}, never_extract = {closedMine n}"

Run lake build && .lake/build/bin/repro. myIsExclusive is the same extern with @[never_extract] added.

Expected behavior
isExclusiveUnsafe: before share = true, after share = false

After IO.mkRef a, a has two references, so the second check must return false, which is what the @[never_extract] copy returns.

Actual behavior
isExclusiveUnsafe: before share = true, after share = true
never_extract    : before share = true, after share = false
closed: core = false, never_extract = false

In trace.compiler.ir.result, coreImpl makes a single isExclusiveUnsafe call, before the inc/mkRef, and boxes its result for both components:

def coreImpl (x_1 : obj) (x_2 : void) : obj :=
  let x_3 : u8 := isExclusiveUnsafe ◾ x_1;
  inc x_1;
  let x_4 : tobj := ST.Prim.mkRef ◾ ◾ x_1 ◾;
  ...
  let x_7 : tobj := box x_3;

closedCoreImpl gets _closed_1 : u8 := isExclusiveUnsafe ◾ _closed_0, which is evaluated once.

Versions

Lean 4.36.0-rc1, 4.35.0 and 4.36.0-nightly-2026-10-12 (commit db7f10e9), on x86_64-unknown-linux-gnu.

Additional Information

Proposed fix: mark isExclusiveUnsafe, and perhaps ptrAddrUnsafe, as @[never_extract].

Note: under #eval, the interpreter seems to hold an extra reference to the argument, so it prints (false, false) there. The bug only shows in compiled code.

[ ] Impact: Add 👍 to issues you consider important. If others are impacted by this issue, please add 👍 to it.

Dominant language
Lean
Stars
9.6k
Forks
1.1k
Avg merge
1d 17m
Merged PRs (30d)
296

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More Compilers issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.