From db35f98b26ffd044727d518fb2f260071eff6956 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 2 Sep 2025 16:36:08 +0200
Subject: [PATCH] fix: make csimp equivalence criteria more strict (#10214)

This PR fixes #10213.
---
 src/Lean/Compiler/CSimpAttr.lean |  7 ++++---
 tests/lean/run/10213.lean        | 23 +++++++++++++++++++++++
 2 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/10213.lean

diff --git a/src/Lean/Compiler/CSimpAttr.lean b/src/Lean/Compiler/CSimpAttr.lean
index c6d1b1c198..130aa6d503 100644
--- a/src/Lean/Compiler/CSimpAttr.lean
+++ b/src/Lean/Compiler/CSimpAttr.lean
@@ -37,10 +37,11 @@ builtin_initialize ext : SimpleScopedEnvExtension Entry State ←
   }
 
 private def isConstantReplacement? (declName : Name) : CoreM (Option Entry) := do
-  let info ← getConstInfo declName
+  let info ← getConstVal declName
   match info.type.eq? with
-  | some (_, Expr.const fromDeclName us .., Expr.const toDeclName vs ..) =>
-    if us == vs then
+  | some (_, Expr.const fromDeclName us, Expr.const toDeclName vs) =>
+    let set := Std.HashSet.ofList us
+    if set.size == us.length && set.all Level.isParam && us == vs then
       return some { fromDeclName, toDeclName, thmName := declName }
     else
       return none
diff --git a/tests/lean/run/10213.lean b/tests/lean/run/10213.lean
new file mode 100644
index 0000000000..46543446c4
--- /dev/null
+++ b/tests/lean/run/10213.lean
@@ -0,0 +1,23 @@
+/-!
+Tests that `@[csimp]` rejects constant replacements with concrete universe parameters
+-/
+
+noncomputable def funnyChoice (x : α) : α := Classical.choice ⟨x⟩
+
+/--
+error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.
+-/
+#guard_msgs in
+@[csimp]
+theorem bad_csimp : @funnyChoice.{0} = @id.{0} := rfl
+
+/--
+error: Tactic `native_decide` failed: Could not evaluate decidable instance. Error: (interpreter) unknown declaration '_example._nativeDecide_1'
+---
+error: failed to compile definition, compiler IR check failed at `_example._nativeDecide_1._closed_0`. Error: depends on declaration 'funnyChoice', which has no executable code; consider marking definition as 'noncomputable'
+-/
+#guard_msgs in
+example : False := by
+  have : funnyChoice 2 = funnyChoice 3 := rfl
+  have : funnyChoice 2 ≠ funnyChoice 3 := by native_decide
+  contradiction