Import failed, environment already contains `sparseCasesOn_2`

[TwoFX]

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

Consider a project Repro with four files:

Repro/A.lean:

module

def a (_ : Unit) : Nat :=
  match some 0 with
  | some _ => 2
  | _ => 2

Repro/B1.lean:

module

import all Repro.A

theorem foo : a () ≠ 1 := by
  fun_cases a with simp

Repro/B2.lean:

module

import all Repro.A

theorem bar : a () ≠ 1 := by
  fun_cases a with simp

Repro/C.lean:

module

import all Repro.B1
import all Repro.B2

Then the file C.lean fails with

import Repro.B2 failed, environment already contains '_private.Repro.A.0.a.match_1.congr_eq_1._sparseCasesOn_2' from Repro.B1

Workaround: add import Repro.B1 to B2.lean.

Context

Originally observed in #12793 where I applied the workaround described above.

Expected behavior: No error.

Actual behavior: See above.

Versions

leanprover/lean4:nightly-2026-03-05
Linux 6.18.13 #1-NixOS SMP PREEMPT_DYNAMIC Thu Feb 19 15:31:37 UTC 2026 x86_64 GNU/Linux

Impact

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

[nomeata]

Some probably related fishiness: Accessing the .splitter uses the existing sparseCasesOn (good), but after generation of the induction principle that's no longer the case:

module

import all Init.Data.String.Slice

set_option pp.notation false
set_option pp.privateNames true

/--
info: private def String.Slice.dropEndWhile.go.match_1.splitter.{u_1} : (s : String.Slice) →
  (curr : s.Pos) →
    (motive : Option (s.sliceTo curr).Pos → Sort u_1) →
      (x : Option (s.sliceTo curr).Pos) →
        ((nextCurr : (s.sliceTo curr).Pos) → motive (some nextCurr)) →
          ((x : Option (s.sliceTo curr).Pos) →
              (∀ (nextCurr : (s.sliceTo curr).Pos), Eq x (some nextCurr) → False) → motive x) →
            motive x :=
fun s curr motive x h_1 h_2 =>
  _private.Init.Data.String.Slice.0.String.Slice.dropWhile.go._sparseCasesOn_1 x (fun val => h_1 val) fun h => h_2 x ⋯
-/
#guard_msgs in
#print String.Slice.dropEndWhile.go.match_1.splitter

def foo := @String.Slice.dropEndWhile.go.induct

/--
info: private def String.Slice.dropEndWhile.go.match_1.splitter.{u_1} : (s : String.Slice) →
  (curr : s.Pos) →
    (motive : Option (s.sliceTo curr).Pos → Sort u_1) →
      (x : Option (s.sliceTo curr).Pos) →
        ((nextCurr : (s.sliceTo curr).Pos) → motive (some nextCurr)) →
          ((x : Option (s.sliceTo curr).Pos) →
              (∀ (nextCurr : (s.sliceTo curr).Pos), Eq x (some nextCurr) → False) → motive x) →
            motive x :=
fun s curr motive x h_1 h_2 =>
  _private.«external:file:///MathlibDemo/MathlibDemo.lean».0.String.Slice.dropEndWhile.go.match_1.splitter._sparseCasesOn_2
    x (fun val => h_1 val) fun h => h_2 x ⋯
-/
#guard_msgs in
#print String.Slice.dropEndWhile.go.match_1.splitter

[nomeata]

The behavior shown here is actually expected: the splitter is intentionally generated on-demand per module as a private declaration (to avoid exactly the import conflicts that are the main issue here). So after @induct triggers realization of the induction principle, which in turn calls getEquationsFor, a new splitter is created under the current module's private prefix. The second #print then finds this new splitter via resolvePrivateName (which prefers the current module's private prefix).

The different _sparseCasesOn index (_2 vs _1) is because during the splitter's realization, the equation theorems are created first (via addDecl → wrapAsyncAsSnapshot → mkChild), which advances the DeclNameGenerator.idx before mkSparseCasesOn runs.

An actual UX issue here is that set_option pp.privateNames true does not affect the name printed in the signature line of #print — only the body. If it did, one would see that the two #print outputs refer to splitters in different modules, making the behavior much less confusing.

— claude