fix: simp only should break Char literals

closes #3686

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -54,6 +54,10 @@ def foldRawNatLit (e : Expr) : SimpM Expr := do
 def isOfScientificLit (e : Expr) : Bool :=
   e.isAppOfArity ``OfScientific.ofScientific 5 && (e.getArg! 4).isRawNatLit && (e.getArg! 2).isRawNatLit
 
+/-- Return true if `e` is of the form `Char.ofNat n` where `n` is a kernel Nat literals. -/
+def isCharLit (e : Expr) : Bool :=
+  e.isAppOfArity ``Char.ofNat 1 && e.appArg!.isRawNatLit
+
 private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
   matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do
     match (← getProjectionFnInfo? cinfo.name) with
@@ -436,13 +440,18 @@ Auliliary `dsimproc` for not visiting `OfScientific.ofScientific` application su
 -/
 private def doNotVisitOfScientific : DSimproc := doNotVisit isOfScientificLit ``OfScientific.ofScientific
 
+/--
+Auliliary `dsimproc` for not visiting `Char` literal subterms.
+-/
+private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
+
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
   unless cfg.dsimp do
     return e
   let m ← getMethods
-  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific
+  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
   let post := m.dpost >> dsimpReduce
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
@@ -562,7 +571,7 @@ def congr (e : Expr) : SimpM Result := do
     congrDefault e
 
 def simpApp (e : Expr) : SimpM Result := do
-  if isOfNatNatLit e || isOfScientificLit e then
+  if isOfNatNatLit e || isOfScientificLit e || isCharLit e then
     -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
     return { expr := e }
   else

tests/lean/run/3686.lean

@@ -0,0 +1,34 @@
+set_option pp.coercions false -- Show `OfNat.ofNat` for clarity
+set_option pp.natLit true -- Show `nat_lit` for clarity
+
+/--
+error: simp made no progress
+-/
+#guard_msgs (error) in
+example (_ : 'a' = x) : 'a' = x := by
+  guard_target =ₛ 'a' = x
+  simp only
+
+/--
+error: simp made no progress
+-/
+#guard_msgs (error) in
+example : 'a' = x := by
+-- ⊢ 'a' = x
+  simp -- error (as expected): simp made no progress
+
+/--
+error: dsimp made no progress
+-/
+#guard_msgs (error) in
+example (_ : 'a' = x) : 'a' = x := by
+  guard_target =ₛ 'a' = x
+  dsimp only
+
+/--
+error: dsimp made no progress
+-/
+#guard_msgs (error) in
+example : 'a' = x := by
+-- ⊢ 'a' = x
+  dsimp -- error (as expected): simp made no progress