`Sym.Simp.EvalGround` produces kernel-rejected proofs when typeclass instances are shadowed

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

The ground-evaluation simprocs in Lean.Meta.Sym.Simp.EvalGround produce proofs that the kernel rejects when the typeclass instance for the operation in question has been shadowed. This affects sym => simp directly and, transitively, cbv (which uses Sym.simp).

Context

Discovered while working on a Lean development that imports Mathlib, which defines String.LT' in Mathlib/Data/String/Basic.lean. Minimised from an example given by @oeb25.

import Mathlib.Data.String.Basic

/--
error: (kernel) application type mismatch
  Eq.mpr (Lean.Sym.String.lt_eq_true "a" "b" (eagerReduce (Eq.refl true)))
argument has type
  ("a" < "b") = True
but function has type
  ("a" < "b") = True → True → "a" < "b"
-/
#guard_msgs in
example : "a" < "b" := by sym => simp

Steps to Reproduce

Here is a Mathlib-free MWE that triggers the same issue on the latest nightly:

  section LT_String
  instance String.LT' : LT String := ⟨fun a b => a.length < b.length⟩
  example : ("a" : String) < "b" := by sym => simp
  end LT_String

  section LE_String
  instance String.LE' : LE String := ⟨fun a b => a.length ≤ b.length⟩
  example : ("a" : String) ≤ "b" := by sym => simp
  end LE_String

  section LT_Char
  instance Char.LT' : LT Char := ⟨fun a b => a.toNat % 2 < b.toNat % 2⟩
  example : ('a' : Char) < 'b' := by sym => simp
  end LT_Char

  section LT_Nat
  instance Nat.LT' : LT Nat := ⟨fun a b => a = 0 ∧ b = 0⟩
  example : (1 : Nat) < 2 := by sym => simp
  end LT_Nat

  section LT_Int
  instance Int.LT' : LT Int := ⟨fun a b => b < a⟩
  example : (1 : Int) < 2 := by sym => simp
  end LT_Int

  section LT_BitVec
  instance (priority := high) BitVec.LT' (n : Nat) : LT (BitVec n) :=
    ⟨fun a b => a.toNat % 7 < b.toNat % 7⟩
  example : (3 : BitVec 8) < 100 := by sym => simp
  end LT_BitVec

  section LT_Fin
  instance (priority := high) Fin.LT' (n : Nat) : LT (Fin n) :=
    ⟨fun a b => a.val % 7 = b.val % 7⟩
  example : (1 : Fin 10) < 8 := by sym => simp
  end LT_Fin

  section HAdd_Nat
  instance (priority := high) Nat.HAdd' : HAdd Nat Nat Nat := ⟨fun _ _ => 42⟩
  example : (1 + 2 : Nat) = 3 := by sym => simp
  end HAdd_Nat

  section HSub_Nat
  instance (priority := high) Nat.HSub' : HSub Nat Nat Nat := ⟨fun _ _ => 0⟩
  example : ((5 : Nat) - 3) = 2 := by sym => simp
  end HSub_Nat

  section HMul_Nat
  instance (priority := high) Nat.HMul' : HMul Nat Nat Nat := ⟨fun a _ => a⟩
  example : (3 * 4 : Nat) = 12 := by sym => simp
  end HMul_Nat

  section HDiv_Nat
  instance (priority := high) Nat.HDiv' : HDiv Nat Nat Nat := ⟨fun _ _ => 0⟩
  example : ((10 : Nat) / 2) = 5 := by sym => simp
  end HDiv_Nat

  section HMod_Nat
  instance (priority := high) Nat.HMod' : HMod Nat Nat Nat := ⟨fun _ _ => 0⟩
  example : ((10 : Nat) % 3) = 1 := by sym => simp
  end HMod_Nat

  section Neg_Int
  instance (priority := high) Int.Neg' : Neg Int := ⟨fun _ => 999⟩
  example : (- (5 : Int)) = -5 := by sym => simp
  end Neg_Int

  section HAnd_Nat
  instance (priority := high) Nat.HAnd' : HAnd Nat Nat Nat := ⟨fun _ _ => 0⟩
  example : ((5 : Nat) &&& 3) = 1 := by sym => simp
  end HAnd_Nat

Expected behavior:
The examples above do not trigger kernel type mismatch.

Actual behavior:
A kernel type mismatch is triggered.

Versions

4.30.0-rc2 (for Mathlib example) and Lean 4.31.0-nightly-2026-04-27 (for Mathlib-free example).

Impact

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

Start in Lean.Meta.Sym.Simp.EvalGround and reproduce the issue with the Mathlib-free examples, especially the shadowed LT and arithmetic instances. The work is done when these examples no longer produce kernel type mismatches through sym => simp, including the transitive cbv behavior described in the issue.