feat: add hints for tuple projections (#9387)

This PR adds a hint to the "invalid projection" message suggesting the
correct nested projection for expressions of the form `t.n` where `t` is
a tuple and `n > 2`.

This feature was originally proposed by @nomeata in #8986.

src/Lean/Elab/App.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Util.FindMVar
 import Lean.Util.CollectFVars
 import Lean.Parser.Term
+import Lean.Meta.Hint
 import Lean.Meta.KAbstract
 import Lean.Meta.Tactic.ElimInfo
 import Lean.Elab.Term
@@ -1289,6 +1290,36 @@ private partial def findMethod? (structName fieldName : Name) : MetaM (Option (N
 private def throwInvalidFieldNotation (e eType : Expr) : TermElabM α :=
   throwLValError e eType "Invalid field notation: Type is not of the form `C ...` where C is a constant"
 
+/--
+If it seems that the user may be attempting to project out the `n`th element of a tuple, or that the
+nesting behavior of n-ary products is otherwise relevant, generates a corresponding hint; otherwise,
+produces an empty message.
+-/
+private partial def mkTupleHint (eType : Expr) (idx : Nat) (ref : Syntax) : TermElabM MessageData := do
+  let arity := prodArity eType
+  if arity > 1 then
+    let numComps := arity + 1
+    if idx ≤ numComps && ref.getHeadInfo matches .original .. then
+      let ordinalSuffix := match idx % 10 with
+        | 1 => "st" | 2 => "nd" | 3 => "rd" | _ => "th"
+      let mut projComps := List.replicate (idx - 1) "2"
+      if idx < numComps then projComps := projComps ++ ["1"]
+      let proj := ".".intercalate projComps
+      let sug := { suggestion := proj, span? := ref,
+                   toCodeActionTitle? := some (s!"Change projection `{idx}` to `{·}`") }
+      MessageData.hint m!"n-tuples in Lean are actually nested pairs. To access the \
+        {idx}{ordinalSuffix} component of this tuple, use the projection `.{proj}` instead:" #[sug]
+    else
+      return MessageData.hint' m!"n-tuples in Lean are actually nested pairs. For example, to access the \
+        \"third\" component of `(a, b, c)`, write `(a, b, c).2.2` instead of `(a, b, c).3`."
+  else
+    return MessageData.nil
+where
+  prodArity (type : Expr) :=
+    match type.prod? with
+    | none => 0
+    | some (_, p2) => prodArity p2 + 1
+
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
   if eType.isForall then
     match lval with
@@ -1312,7 +1343,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       | .fieldIdx _ i => (m!"projection", m!"projection `{i}`")
     throwError "Invalid {kind}: Type of{indentExpr e}\nis not known; cannot resolve {name}"
   match eType.getAppFn.constName?, lval with
-  | some structName, LVal.fieldIdx _ idx =>
+  | some structName, LVal.fieldIdx ref idx =>
     if idx == 0 then
       throwError "Invalid projection: Index must be greater than 0"
     let env ← getEnv
@@ -1335,8 +1366,10 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           (m!"field", m!"the only valid index is 1")
         else
           (m!"fields", m!"it must be between 1 and {numFields}")
+        let tupleHint ← mkTupleHint eType idx ref
         throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; {bounds}"
           ++ .note m!"The expression{inlineExpr e}has type{inlineExpr eType}which has only {numFields} {fields}"
+          ++ tupleHint
   | some structName, LVal.fieldName _ fieldName _ fullRef =>
     let env ← getEnv
     if isStructure env structName then
@@ -1385,7 +1418,7 @@ private partial def consumeImplicits (stx : Syntax) (e eType : Expr) (hasArgs :
       | _ => return (e, eType)
   | _ => return (e, eType)
 
-private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExceptions : Array Exception) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do
+private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do
   let (e, eType) ← consumeImplicits lval.getRef e eType hasArgs
   tryPostponeIfMVar eType
   /- If `eType` is still a metavariable application, we try to apply default instances to "unblock" it. -/
@@ -1399,15 +1432,13 @@ private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExce
     | ex@(Exception.error _ _) =>
       let eType? ← unfoldDefinition? eType
       match eType? with
-      | some eType => resolveLValLoop lval e eType (previousExceptions.push ex) hasArgs
-      | none       =>
-        previousExceptions.forM fun ex => logException ex
-        throw ex
+      | some eType => resolveLValLoop lval e eType hasArgs
+      | none       => throw ex
     | ex@(Exception.internal _ _) => throw ex
 
 private def resolveLVal (e : Expr) (lval : LVal) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do
   let eType ← inferType e
-  resolveLValLoop lval e eType #[] hasArgs
+  resolveLValLoop lval e eType hasArgs
 
 private partial def mkBaseProjections (baseStructName : Name) (structName : Name) (e : Expr) : TermElabM Expr := do
   let env ← getEnv

tests/lean/run/invalidProjection.lean

@@ -21,6 +21,9 @@ example (h1 : P n h) (h2 : P m h') := h1.1 = h2.2
 error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2
 
 Note: The expression `x` has type `Nat × Nat × Nat` which has only 2 fields
+
+Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead:
+  3̵2̲.̲2̲
 -/
 #guard_msgs in
 example (x : Nat × Nat × Nat) := x.3

tests/lean/run/invalidTupleProjHints.lean

@@ -0,0 +1,70 @@
+/-!
+# Hints for invalid tuple projections
+
+These tests assess hints for invalid projections that may be incorrectly attempting to project the
+`n`th element from a tuple where `n > 2`.
+-/
+
+def p : Nat × Nat × Nat := (3, 4, 5)
+/--
+error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2
+
+Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields
+
+Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead:
+  3̵2̲.̲2̲
+-/
+#guard_msgs in
+#check p.3
+
+/--
+error: Invalid projection: Index `17` is invalid for this structure; it must be between 1 and 2
+
+Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields
+
+Hint: n-tuples in Lean are actually nested pairs. For example, to access the "third" component of `(a, b, c)`, write `(a, b, c).2.2` instead of `(a, b, c).3`.
+-/
+#guard_msgs in
+#check p.17
+
+/--
+error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2
+
+Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields
+
+Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead:
+  3̵2̲.̲2̲
+-/
+#guard_msgs in
+#check p.3.succ
+
+/-
+In prior versions of Lean, the below would erroneously produce two error messages: "structure type
+expected" on the first lval resolution iteration (prior to unfolding `MyProd`), then (correctly)
+"invalid index" on the second, post-unfolding iteration
+-/
+abbrev MyProd := Nat × Nat × Nat × Nat × Nat
+def mp : MyProd := (1, 2, 3, 4, 5)
+/--
+error: Invalid projection: Index `4` is invalid for this structure; it must be between 1 and 2
+
+Note: The expression `mp` has type `Nat × Nat × Nat × Nat × Nat` which has only 2 fields
+
+Hint: n-tuples in Lean are actually nested pairs. To access the 4th component of this tuple, use the projection `.2.2.2.1` instead:
+  4̵2̲.̲2̲.̲2̲.̲1̲
+-/
+#guard_msgs in
+#eval mp.4
+
+-- Ensure we don't produce hints for synthetic syntax
+macro "illegally_project_from_a_tuple" : term => `((true, true, false).3)
+
+/--
+error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2
+
+Note: The expression `(true, true, false)` has type `Bool × Bool × Bool` which has only 2 fields
+
+Hint: n-tuples in Lean are actually nested pairs. For example, to access the "third" component of `(a, b, c)`, write `(a, b, c).2.2` instead of `(a, b, c).3`.
+-/
+#guard_msgs in
+#check illegally_project_from_a_tuple