Kernel failed to type-check due to name collision involving `include`

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Under the following conditions, we get an error in the kernel:

• two variables, one depending on another
• the dependent one is included, transitively includeing its dependency
• there is a local variable with the same name as the dependency
• the included variables are not used in the declaration

Steps to Reproduce

The following code errors:

variables (a : ℕ)
variables (ha : a = a)

include ha

theorem ex (a : ℕ) : a = a := rfl

/-
error:
kernel failed to type check declaration 'ex' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  a = a → ℕ → ∀ (a : ℕ), a = a
elaborated value:
  λ (ha : a = a) (a a : ℕ), rfl
nested exception message:
failed to add declaration to environment, it contains local constants
-/

Expected behavior: No errors in the kernel, like when there's no name clash.

Actual behavior: An error:

error:
kernel failed to type check declaration 'ex' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  a = a → ℕ → ∀ (a : ℕ), a = a
elaborated value:
  λ (ha : a = a) (a a : ℕ), rfl
nested exception message:
failed to add declaration to environment, it contains local constants

Reproduces how often: always

Versions

Lean (version 3.45.0, commit 22b09be35ef6, Release)

Start with the self-contained Lean reproducer under Lean 3.45.0, focusing on the interaction between dependent variables, transitive include, and the local name collision. Done means the declaration type-checks without the kernel reporting local constants in the environment, while the no-name-clash case continues to work.