fix: improve hint diffs

Author: jrr6

src/Lean/Message.lean

@@ -349,16 +349,14 @@ def andList (xs : List MessageData) : MessageData :=
 Produces a labeled note that can be appended to an error message.
 -/
 def note (note : MessageData) : MessageData :=
-  -- Note: we do not use the built-in string coercion because it can prevent proper line breaks
-  -- FIXME: doing this doesn't end the enclosing group, so line feeds in `note` may become spaces
-  "\n" ++ "\n" ++ "Note: " ++ note
+  Format.line ++ Format.line ++ "Note: " ++ note
 
 /--
 Produces a labeled hint without an associated code action (non-monadic variant of
 `MessageData.hint`).
 -/
 def hint' (hint : MessageData) : MessageData :=
-  .ofFormat "\n\nHint: " ++ hint
+  Format.line ++ Format.line ++ "Hint: " ++ hint
 
 instance : Coe (List MessageData) MessageData := ⟨ofList⟩
 instance : Coe (List Expr) MessageData := ⟨fun es => ofList <| es.map ofExpr⟩

src/Lean/Meta/Hint.lean

@@ -11,6 +11,7 @@ import Lean.Data.Lsp.Utf16
 import Lean.Message
 import Lean.Meta.TryThis
 import Lean.Util.Diff
+import Lean.Util.EditDistance
 import Lean.Widget.Types
 import Lean.PrettyPrinter
 
@@ -66,48 +67,43 @@ export default function ({ diff, range, suggestion }) {
       e('span', defStyle, comp.text)
   )
   const fullDiff = e('span',
-    { onClick, title: 'Apply suggestion', className: 'link pointer dim font-code', },
+    { onClick,
+      title: 'Apply suggestion',
+      className: 'link pointer dim font-code',
+      style: { display: 'inline-block', verticalAlign: 'text-top' } },
     spans)
   return fullDiff
 }"
 
 /--
 Converts an array of diff actions into corresponding JSON interpretable by `tryThisDiffWidget`.
 -/
-private def mkDiffJson (ds : Array (Diff.Action × Char)) :=
-  -- Avoid cluttering the DOM by grouping "runs" of the same action
-  let unified : List (Diff.Action × List Char) := ds.foldr (init := []) fun
-    | (act, c), [] => [(act, [c])]
-    | (act, c), (act', cs) :: acc =>
-      if act == act' then
-        (act, c :: cs) :: acc
-      else
-        (act, [c]) :: (act', cs) :: acc
-  toJson <| unified.map fun
-    | (.insert, s) => json% { type: "insertion", text: $(String.mk s) }
-    | (.delete, s) => json% { type: "deletion", text: $(String.mk s) }
-    | (.skip  , s) => json% { type: "unchanged", text: $(String.mk s) }
+private def mkDiffJson (ds : Array (Diff.Action × String)) :=
+  toJson <| ds.map fun
+    | (.insert, s) => json% { type: "insertion", text: $s }
+    | (.delete, s) => json% { type: "deletion", text: $s }
+    | (.skip  , s) => json% { type: "unchanged", text: $s }
 
 /--
 Converts an array of diff actions into a Unicode string that visually depicts the diff.
 
 Note that this function does not return the string that results from applying the diff to some
-input; rather, it returns a string representation of the actions that the diff itself comprises, such as `b̵a̵c̲h̲e̲e̲rs̲`.
-
+input; rather, it returns a string representation of the actions that the diff itself comprises,
+such as `b̵a̵c̲h̲e̲e̲rs̲`.
 -/
-private def mkDiffString (ds : Array (Diff.Action × Char)) : String :=
+private def mkDiffString (ds : Array (Diff.Action × String)) : String :=
   let rangeStrs := ds.map fun
-    | (.insert, s) => String.mk [s, '\u0332'] -- U+0332 Combining Low Line
-    | (.delete, s) => String.mk [s, '\u0335'] -- U+0335 Combining Short Stroke Overlay
-    | (.skip  , s) => String.mk [s]
+    | (.insert, s) => String.mk (s.data.flatMap ([·, '\u0332'])) -- U+0332 Combining Low Line
+    | (.delete, s) => String.mk (s.data.flatMap ([·, '\u0335'])) -- U+0335 Combining Short Stroke Overlay
+    | (.skip  , s) => s
   rangeStrs.foldl (· ++ ·) ""
 
 /--
 A code action suggestion associated with a hint in a message.
 
 Refer to `TryThis.Suggestion`; this extends that structure with a `span?` field, allowing a single
-hint to suggest modifications at different locations. If `span?` is not specified, then the `ref`
-for the containing `Suggestions` value is used.
+hint to suggest modifications at different locations. If `span?` is not specified, then the syntax
+reference provided to `MessageData.hint` will be used.
 -/
 structure Suggestion extends TryThis.Suggestion where
   span? : Option Syntax := none
@@ -119,40 +115,83 @@ instance : ToMessageData Suggestion where
   toMessageData s := toMessageData s.toSuggestion
 
 /--
-A collection of code action suggestions to be included in a hint in a diagnostic message.
+Produces a diff that splits either on characters, tokens, or not at all, depending on the edit
+distance between the arguments.
 
-Contains the following fields:
-* `ref`: the syntax location for the code action suggestions. Will be overridden by the `span?`
-  field on any suggestions that specify it.
-* `suggestions`: the suggestions to display.
-* `codeActionPrefix?`: if specified, text to display in place of "Try this: " in the code action
-  label
+Guarantees that all actions in the output will be maximally grouped; that is, instead of returning
+`#[(.insert, "a"), (.insert, "b")]`, it will return `#[(.insert, "ab")]`.
 -/
-structure Suggestions where
-  ref : Syntax
-  suggestions : Array Suggestion
-  codeActionPrefix? : Option String := none
+def readableDiff (s s' : String) : Array (Diff.Action × String) :=
+  let minLength := min s.length s'.length
+  -- Given that `Diff.diff` returns a minimal diff, any length-≤3 diff can only have edits at the
+  -- front and back, or at a single interior point. This will always be fairly readable, so we can
+  -- return it without further analysis:
+  if charDiff.size ≤ 3 then
+    charDiff
+  else
+    -- The coefficients on these two constants can be tuned:
+    let charDiffDistance := minLength / 5
+    let wordDiffDistance := minLength
+    if let some editDistance := EditDistance.levenshtein s s' wordDiffDistance then
+      if editDistance < charDiffDistance then
+        charDiff
+      else
+        wordDiff
+    else
+      maxDiff
+where
+  splitChars (s : String) :=
+    s.toList.toArray
+
+  splitWords (s : String) :=
+    s.splitOn " " |>.intersperse " " |>.toArray
+
+  charDiff :=
+    Diff.diff (splitChars s) (splitChars s')
+      |> joinEdits
+      |>.map fun (act, cs) => (act, String.mk cs.toList)
+
+  wordDiff :=
+    Diff.diff (splitWords s) (splitWords s')
+      |> joinEdits
+      |>.map fun (act, ss) =>  (act, ss.foldl (· ++ ·) "")
+
+  maxDiff :=
+    #[(.delete, s), (.insert, s')]
+
+  joinEdits {α} (ds : Array (Diff.Action × α)) : Array (Diff.Action × Array α) :=
+    ds.foldl (init := #[]) fun acc (act, c) =>
+      if h : acc.isEmpty then
+        #[(act, #[c])]
+      else
+        have : acc.size - 1 < acc.size := Nat.sub_one_lt <| mt Array.size_eq_zero_iff.mp <|
+          Array.isEmpty_eq_false_iff.mp (Bool.of_not_eq_true h)
+        let (act', cs) := acc[acc.size - 1]
+        if act == act' then
+          acc.set (acc.size - 1) (act, cs.push c)
+        else
+          acc.push (act, #[c])
 
 /--
 Creates message data corresponding to a `HintSuggestions` collection and adds the corresponding info
 leaf.
 -/
-def Suggestions.toHintMessage (suggestions : Suggestions) : CoreM MessageData := do
-  let { ref, codeActionPrefix?, suggestions } := suggestions
+def mkSuggestionsMessage (suggestions : Array Suggestion)
+    (ref : Syntax)
+    (codeActionPrefix? : Option String) : CoreM MessageData := do
   let mut msg := m!""
   for suggestion in suggestions do
     if let some range := (suggestion.span?.getD ref).getRange? then
-      let { info, suggestions := suggestionArr, range := lspRange } ← processSuggestions ref range
-        #[suggestion.toSuggestion] codeActionPrefix?
+      let { info, suggestions := suggestionArr, range := lspRange } ←
+        processSuggestions ref range #[suggestion.toSuggestion] codeActionPrefix?
       pushInfoLeaf info
       let suggestionText := suggestionArr[0]!.2.1
       let map ← getFileMap
       let rangeContents := Substring.mk map.source range.start range.stop |>.toString
-      let split (s : String) := s.toList.toArray
-      let edits := Diff.diff (split rangeContents) (split suggestionText)
-      let diff := mkDiffJson edits
+      let edits := readableDiff rangeContents suggestionText
+      let diffJson := mkDiffJson edits
       let json := json% {
-        diff: $diff,
+        diff: $diffJson,
         suggestion: $suggestionText,
         range: $lspRange
       }
@@ -167,15 +206,28 @@ def Suggestions.toHintMessage (suggestions : Suggestions) : CoreM MessageData :=
       let suggestionMsg := if suggestions.size == 1 then
         MessageData.ofFormat "\n" ++ m!"{widgetMsg}"
       else
-        MessageData.ofFormat "\n" ++ m!"• {widgetMsg}"
+        MessageData.ofFormat "\n" ++ MessageData.nest 2 m!"• {widgetMsg}"
       msg := msg ++ MessageData.nestD suggestionMsg
   return msg
 
 /--
-Creates a hint message from `hint` with associated code action(s) given by `suggestions`.
+Creates a hint message with associated code action suggestions.
 
 To provide a hint without an associated code action, use `MessageData.hint'`.
+
+The arguments are as follows:
+* `hint`: the main message of the hint, which precedes its code action suggestions.
+* `suggestions`: the suggestions to display.
+* `ref?`: if specified, the syntax location for the code action suggestions; otherwise, default to
+  the syntax reference in the monadic state. Will be overridden by the `span?` field on any
+  suggestions that specify it.
+* `codeActionPrefix?`: if specified, text to display in place of "Try this: " in the code action
+  label
 -/
-def _root_.Lean.MessageData.hint (hint : MessageData) (suggestions : Suggestions)
+def _root_.Lean.MessageData.hint (hint : MessageData)
+    (suggestions : Array Suggestion) (ref? : Option Syntax := none)
+    (codeActionPrefix? : Option String := none)
     : CoreM MessageData := do
-  return .tagged `hint (.ofFormat "\n\nHint: " ++ hint ++ (← suggestions.toHintMessage))
+  let ref := ref?.getD (← getRef)
+  let suggs ← mkSuggestionsMessage suggestions ref codeActionPrefix?
+  return .tagged `hint (m!"\n\nHint: " ++ hint ++ suggs)

src/Lean/Util.lean

@@ -8,6 +8,7 @@ import Lean.Util.CollectFVars
 import Lean.Util.CollectLevelParams
 import Lean.Util.CollectMVars
 import Lean.Util.CollectLevelMVars
+import Lean.Util.EditDistance
 import Lean.Util.FindMVar
 import Lean.Util.FindLevelMVar
 import Lean.Util.MonadCache

src/Lean/Util/Diff.lean

@@ -20,7 +20,7 @@ inductive Action where
   | delete
   /-- Leave the item in the source -/
   | skip
-deriving Repr, BEq, Hashable, Repr
+deriving Repr, BEq, Hashable, Inhabited
 
 instance : ToString Action where
   toString

src/Lean/Util/EditDistance.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+set_option linter.missingDocs true
+
+namespace Lean.EditDistance
+
+/--
+Compute the Levenshtein distance between two strings, up to some cutoff.
+
+If the return value is `none`, then the distance is certainly greater than the cutoff value, but a
+returned `some` does not necessarily indicate that the edit distance is less than or equal to the
+cutoff.
+-/
+def levenshtein (str1 str2 : String) (cutoff : Nat) : Option Nat := Id.run do
+  let len1 := str1.length
+  let len2 := str2.length
+
+  -- The lower bound on the Levenshtein distance is the difference in lengths
+  if max len1 len2 - min len1 len2 > cutoff then return none
+
+  let mut v0 := Array.replicate (len2 + 1) 0
+  let mut v1 := v0
+
+  for i in [0:v0.size] do
+    v0 := v0.set! i i
+  let mut iter1 := str1.iter
+  for i in [0:str1.length] do
+    v1 := v1.set! 0 (i+1)
+    let mut iter2 := str2.iter
+    for j in [0:len2] do
+      let deletionCost := v0[j+1]! + 1
+      let insertionCost := v1[j]! + 1
+      let substCost :=
+        if iter1.curr == iter2.curr then v0[j]!
+        else v0[j]! + 1
+      let cost := min (min deletionCost insertionCost) substCost
+      v1 := v1.set! (j+1) cost
+      iter2 := iter2.next
+    iter1 := iter1.next
+    -- Terminate early if it's impossible that the result is below the cutoff
+    if v1.all (· > cutoff) then return none
+    v0 := v1
+  some v0[len2]!