fix: make csimp equivalence criteria more strict (#10214)

This PR fixes #10213.

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

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