fix: reduce ambiguity of "final" in application type mismatch message (#8322)

This PR refines the new wording of the "application type mismatch" error
message to avoid ambiguity in references to the "final" argument in a
subexpression that may be followed by additional arguments.

It does so by replacing "final" with "last," rephrasing the message so
that this adjective modifies the argument itself rather than the word
"argument," and only displaying this wording when two arguments could be
confused (determined by expression equality).

These changes were motivated by a report that in cases where a function
application `f a b c` fails to elaborate because `b` is incorrectly
typed, the existing error message's reference to `b` being the "final"
argument in the application `f a b` may create confusion because it is
not the final argument in the full application expression.

Author: jrr6

src/Lean/Meta/Check.lean

@@ -209,7 +209,14 @@ def throwAppTypeMismatch (f a : Expr) : MetaM α := do
   unless binfo.isExplicit do
     e := e.setAppPPExplicit
   let aType ← inferType a
-  throwError "Application type mismatch: In the application{indentExpr e}\nthe final argument{indentExpr a}\n{← mkHasTypeButIsExpectedMsg aType expectedType}"
+  -- Clarify that `a` is "last" only if it may be confused with some preceding argument; otherwise,
+  -- avoid this wording because it may be misleading if more arguments follow `a`, e.g., if `f a` is
+  -- a subexpression of `f a b`
+  let argDescStr := if f.getAppArgs.any (· == a) then
+    m!"last{indentExpr a}\nargument "
+  else
+    m!"argument{indentExpr a}\n"
+  throwError "Application type mismatch: In the application{indentExpr e}\nthe {argDescStr}{← mkHasTypeButIsExpectedMsg aType expectedType}"
 
 def checkApp (f a : Expr) : MetaM Unit := do
   let fType ← inferType f

tests/lean/243.lean.expected.out

@@ -1,14 +1,14 @@
 243.lean:2:10-2:14: error: Application type mismatch: In the application
   ⟨Bool, true⟩
-the final argument
+the argument
   true
 has type
   _root_.Bool : Type
 but is expected to have type
   Bool : Type
 243.lean:13:7-13:8: error: Application type mismatch: In the application
   ⟨A, a⟩
-the final argument
+the argument
   a
 has type
   Foo.A : Type

tests/lean/283.lean.expected.out

@@ -1,6 +1,6 @@
 283.lean:1:24-1:25: error: Application type mismatch: In the application
   f f
-the final argument
+the argument
   f
 has type
   ?m : Sort ?u

tests/lean/389.lean.expected.out

@@ -1,6 +1,6 @@
 389.lean:7:14-7:17: error: Application type mismatch: In the application
   getFoo bar
-the final argument
+the argument
   bar
 has type
   Bar Nat : Type

tests/lean/423.lean.expected.out

@@ -1,30 +1,30 @@
 423.lean:3:35-3:40: error: Application type mismatch: In the application
   HAdd.hAdd a
-the final argument
+the argument
   a
 has type
   T : Sort u
 but is expected to have type
   Nat : Type
 423.lean:5:37-5:38: error: Application type mismatch: In the application
   Add T
-the final argument
+the argument
   T
 has type
   Sort u : Type u
 but is expected to have type
   Type ?u : Type (?u + 1)
 423.lean:5:47-5:48: error: Application type mismatch: In the application
   OfNat T
-the final argument
+the argument
   T
 has type
   Sort u : Type u
 but is expected to have type
   Type ?u : Type (?u + 1)
 423.lean:5:55-5:60: error: Application type mismatch: In the application
   HAdd.hAdd a
-the final argument
+the argument
   a
 has type
   T : Sort u

tests/lean/autoPPExplicit.lean.expected.out

@@ -1,6 +1,6 @@
 autoPPExplicit.lean:2:26-2:31: error: Application type mismatch: In the application
   @Eq.trans α a (b = c)
-the final argument
+the argument
   b = c
 has type
   Prop : Type

tests/lean/doErrorMsg.lean.expected.out

@@ -30,7 +30,7 @@ but is expected to have type
   ExceptT String (StateT Nat Id) String : Type
 doErrorMsg.lean:28:13-28:18: error: Application type mismatch: In the application
   Prod.mk false
-the final argument
+the argument
   false
 has type
   Bool : Type

tests/lean/doIssue.lean.expected.out

@@ -12,7 +12,7 @@ but is expected to have type
   IO PUnit : Type
 doIssue.lean:18:7-18:20: error: Application type mismatch: In the application
   pure (xs.set! 0 1)
-the final argument
+the argument
   xs.set! 0 1
 has type
   Array Nat : Type

tests/lean/elseifDoErrorPos.lean.expected.out

@@ -1,14 +1,14 @@
 elseifDoErrorPos.lean:4:10-4:11: error: Application type mismatch: In the application
   @ite ?m x
-the final argument
+the argument
   x
 has type
   Nat : Type
 but is expected to have type
   Prop : Type
 elseifDoErrorPos.lean:7:11-7:14: error: Application type mismatch: In the application
   pure "a"
-the final argument
+the argument
   "a"
 has type
   String : Type

tests/lean/evalSorry.lean.expected.out

@@ -1,7 +1,7 @@
 1
 evalSorry.lean:5:33-5:34: error: Application type mismatch: In the application
   f x
-the final argument
+the argument
   x
 has type
   String : Type