feat: add case name hints (#9316)

This PR adds clickable code-action hints to the "invalid case name"
error message.

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Diagnostics
+import Lean.Meta.Hint
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Contradiction
@@ -498,9 +499,9 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
 
 private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do
   let gs ← getUnsolvedGoals
-  let g ← if let `(binderIdent| $tag:ident) := tag then
-    let tag := tag.getId.eraseMacroScopes
-    let some g ← findTag? gs tag | notFound gs tag
+  let g ← if let `(binderIdent| $tagId:ident) := tag then
+    let tagId := tagId.getId.eraseMacroScopes
+    let some g ← findTag? gs tagId | notFound gs tagId tag
     pure g
   else
     getMainGoal
@@ -509,22 +510,31 @@ private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List
 where
   -- When the case tag is not found, construct a message that tells
   -- the user what they could have written
-  notFound (available : List MVarId) (tag : Name) := do
+  notFound (available : List MVarId) (tag : Name) (tagStx : TSyntax ``binderIdent) := do
     let firstLine := m!"Case tag {showTagName tag} not found."
+    let isOriginalStx := tagStx.raw.getHeadInfo matches .original ..
     -- We must filter out the anonymous name because there may be an
     -- anonymous goal, but users shouldn't be mistakenly encouraged
     -- to write `case anonymous`
-    match (← available.mapM getUserName).filter (· ≠ Name.anonymous) with
-    | [] =>
-      throwError "{firstLine}\n\nThere are no cases to select."
-    | [availableName] =>
-      throwError "{firstLine}\n\nThe only available case tag is {showTagName availableName}."
-    | availableNames =>
-      throwError "Case tag {showTagName tag} not found.\n\nAvailable tags:{commaList <| availableNames.map showTagName}"
+    let hint ← match (← available.mapM getUserName).filter (· ≠ Name.anonymous) with
+      | [] => pure <| MessageData.note m!"There are no cases to select."
+      | [availableName] =>
+        let msg := m!"The only available case tag is {showTagName availableName}."
+        if isOriginalStx then
+          MessageData.hint msg (mkSuggestions #[availableName]) (ref? := tagStx)
+        else
+          pure <| MessageData.hint' msg
+      | availableNames =>
+        let msg := "Available tags:"
+        if isOriginalStx then
+          MessageData.hint msg (mkSuggestions availableNames.toArray) (ref? := tagStx)
+        else
+          pure <| MessageData.hint' m!"{msg}{commaList <| availableNames.map showTagName}"
+    throwError firstLine ++ hint
 
   getUserName (mv : MVarId) := do return (← mv.getDecl).userName
 
-  showTagName (tagName : Name) : MessageData := m!"'{tagName}'"
+  showTagName (tagName : Name) : MessageData := m!"`{tagName}`"
 
   -- Construct a comma-separated list that renders one per line,
   -- indented, if it's too long
@@ -533,6 +543,12 @@ where
     .group <| .nest 2 <|
     .ofFormat .line ++ .joinSep items sep
 
+  mkSuggestions (names : Array Name) :=
+    names.map fun name =>
+      { suggestion := name.toString
+        toCodeActionTitle? := some fun s => s!"Change case name: {s}"
+        preInfo? := if names.size == 1 then none else s!"`{name}`: " : Hint.Suggestion }
+
 @[builtin_tactic «case», builtin_incremental]
 def evalCase : Tactic
   | stx@`(tactic| case%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>

tests/lean/caseSuggestions.lean

@@ -43,3 +43,13 @@ def sixteenCases : Nat := by
   cases true <;> cases true <;> cases true <;> cases true
   case nonexistent =>
     skip
+
+/-!
+  This example tests that the code-action hint doesn't appear when the identifier syntax is
+  synthetic.
+-/
+macro "faulty_case_selector " " => " ts:tacticSeq : tactic => `(tactic| case nonexistent => $ts)
+def inapplicableSyntax : Nat := by
+  cases true
+  faulty_case_selector =>
+    skip

tests/lean/caseSuggestions.lean.expected.out

@@ -1,42 +1,52 @@
-caseSuggestions.lean:11:2-12:8: error: Case tag 'nonexistent' not found.
+caseSuggestions.lean:11:2-12:8: error: Case tag `nonexistent` not found.
 
-There are no cases to select.
-caseSuggestions.lean:20:2-21:8: error: Case tag 'nonexistent' not found.
+Note: There are no cases to select.
+caseSuggestions.lean:20:2-21:8: error: Case tag `nonexistent` not found.
 
-The only available case tag is 'unit'.
-caseSuggestions.lean:29:2-30:8: error: Case tag 'nonexistent' not found.
+Hint: The only available case tag is `unit`.
+  n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵u̲n̲i̲t̲
+caseSuggestions.lean:29:2-30:8: error: Case tag `nonexistent` not found.
 
-Available tags: 'false', 'true'
-caseSuggestions.lean:34:2-35:8: error: Case tag 'nonexistent' not found.
+Hint: Available tags:
+  • `false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲
+  • `true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲
+caseSuggestions.lean:34:2-35:8: error: Case tag `nonexistent` not found.
 
-Available tags: 'false.false', 'false.true', 'true.false', 'true.true'
-caseSuggestions.lean:39:2-40:8: error: Case tag 'nonexistent' not found.
+Hint: Available tags:
+  • `false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲
+  • `false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲
+  • `true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲
+  • `true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲
+caseSuggestions.lean:39:2-40:8: error: Case tag `nonexistent` not found.
 
-Available tags:
-  'false.false.false',
-  'false.false.true',
-  'false.true.false',
-  'false.true.true',
-  'true.false.false',
-  'true.false.true',
-  'true.true.false',
-  'true.true.true'
-caseSuggestions.lean:44:2-45:8: error: Case tag 'nonexistent' not found.
+Hint: Available tags:
+  • `false.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲
+  • `false.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲
+  • `false.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲
+  • `false.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲
+  • `true.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲
+  • `true.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲
+  • `true.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲
+  • `true.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲
+caseSuggestions.lean:44:2-45:8: error: Case tag `nonexistent` not found.
 
-Available tags:
-  'false.false.false.false',
-  'false.false.false.true',
-  'false.false.true.false',
-  'false.false.true.true',
-  'false.true.false.false',
-  'false.true.false.true',
-  'false.true.true.false',
-  'false.true.true.true',
-  'true.false.false.false',
-  'true.false.false.true',
-  'true.false.true.false',
-  'true.false.true.true',
-  'true.true.false.false',
-  'true.true.false.true',
-  'true.true.true.false',
-  'true.true.true.true'
+Hint: Available tags:
+  • `false.false.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲
+  • `false.false.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲
+  • `false.false.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲
+  • `false.false.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲
+  • `false.true.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲
+  • `false.true.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲
+  • `false.true.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲
+  • `false.true.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲
+  • `true.false.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲
+  • `true.false.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲
+  • `true.false.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲
+  • `true.false.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲
+  • `true.true.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲
+  • `true.true.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲
+  • `true.true.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲
+  • `true.true.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲
+caseSuggestions.lean:54:2-55:8: error: Case tag `nonexistent` not found.
+
+Hint: Available tags: `false`, `true`

tests/lean/run/allGoals.lean

@@ -141,13 +141,15 @@ even though the metavariable is assigned in the `refine_2.false` case before the
 -/
 set_option pp.mvars false in
 /--
-error: Case tag 'true' not found.
+error: Case tag `true` not found.
 
-The only available case tag is 'refine_2.false'.
+Hint: The only available case tag is `refine_2.false`.
+  t̵r̵u̵e̵r̲e̲f̲i̲n̲e̲_̲2̲.̲f̲a̲l̲s̲e̲
 ---
-error: Case tag 'true' not found.
+error: Case tag `true` not found.
 
-The only available case tag is 'refine_1'.
+Hint: The only available case tag is `refine_1`.
+  t̵r̵u̵e̵r̲e̲f̲i̲n̲e̲_̲1̲
 ---
 trace: case refine_2.false
 v : Unit := ()