Bug in deprecation linter

[abdoo8080]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

I'm getting an unexpected deprecation warning from the snippet below on the latest nightly:

open String in
def test : Unit := Id.run do
  let mut next : Unit := ()
  while false do
    next := ()
  ()

Context

This bug is not specific to String.next. I reproduced it using other deprecated names. Interestingly, the warning disappears if while is replaced with unless (condition does not matter).

Steps to Reproduce

1. Paste the code above into an empty Lean file (online-version).

Expected behavior: No warning

Actual behavior: I get a warning

Versions

No warning: 4.24.0
Warning: 4.25.1
Warning: 4.27.0-nightly-2025-11-30

Additional Information

N/A

Impact

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