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.

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,6 +1,6 @@
 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
@@ -8,7 +8,7 @@ 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,6 +1,6 @@
 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
@@ -8,7 +8,7 @@ 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
@@ -16,7 +16,7 @@ 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
@@ -24,7 +24,7 @@ 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,6 +1,6 @@
 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
@@ -8,7 +8,7 @@ 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

tests/lean/macroSwizzle.lean.expected.out

@@ -4,7 +4,7 @@ macroSwizzle.lean:4:7-4:23: error: failed to synthesize
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 macroSwizzle.lean:6:7-6:10: error: Application type mismatch: In the application
   Nat.succ "x"
-the final argument
+the argument
   "x"
 has type
   String : Type

tests/lean/modBug.lean.expected.out

@@ -1,6 +1,6 @@
 modBug.lean:1:48-1:64: error: Application type mismatch: In the application
   Nat.zero_ne_one (Nat.mod_zero 1)
-the final argument
+the argument
   Nat.mod_zero 1
 has type
   1 % 0 = 1 : Prop

tests/lean/motiveNotTypeCorect.lean.expected.out

@@ -2,7 +2,7 @@ motiveNotTypeCorect.lean:7:6-7:7: error: tactic 'rewrite' failed, motive is not
   fun _a => P _a d
 Error: Application type mismatch: In the application
   P _a d
-the final argument
+the argument
   d
 has type
   D (f t) : Type

tests/lean/nameArgErrorIssue.lean.expected.out

@@ -1,7 +1,7 @@
 bla 5 2 : Nat
 nameArgErrorIssue.lean:5:20-5:24: error: Application type mismatch: In the application
   bla "hi"
-the final argument
+the argument
   "hi"
 has type
   String : Type
@@ -10,7 +10,7 @@ but is expected to have type
 bla sorry 5 : Nat
 nameArgErrorIssue.lean:6:20-6:24: error: Application type mismatch: In the application
   bla "hi"
-the final argument
+the argument
   "hi"
 has type
   String : Type

tests/lean/namedHoles.lean.expected.out

@@ -1,8 +1,8 @@
 namedHoles.lean:9:12-9:14: error: Application type mismatch: In the application
   f ?x ?x
-the final argument
+the last
   ?x
-has type
+argument has type
   Nat : Type
 but is expected to have type
   Bool : Type

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -1,6 +1,6 @@
 phashmap_inst_coherence.lean:12:53-12:54: error: Application type mismatch: In the application
   m.find?
-the final argument
+the argument
   m
 has type
   @PersistentHashMap Nat Nat instBEqOfDecidableEq instHashableNat : Type

tests/lean/run/439.lean

@@ -44,7 +44,7 @@ variable (fn' : Fn ((p : P) -> B.fn p -> B.fn p) ({p : P} -> B.fn p -> B.fn p))
 /--
 error: Application type mismatch: In the application
   fn'.imp p
-the final argument
+the argument
   p
 has type
   P : Sort u

tests/lean/run/4405.lean

@@ -5,7 +5,7 @@ set_option pp.mvars false
 /--
 error: Application type mismatch: In the application
   ⟨Nat.lt_irrefl (?_ n), Fin.is_lt ?_⟩
-the final argument
+the argument
   Fin.is_lt ?_
 has type
   ↑?_ < ?_ : Prop

tests/lean/run/4670.lean

@@ -13,7 +13,7 @@ Was printing `true.out`, but it should have been `Foo.out true`.
 /--
 error: Application type mismatch: In the application
   Foo.out true
-the final argument
+the argument
   true
 has type
   Bool : Type
@@ -31,7 +31,7 @@ def Foo.out' (f : Foo) : Nat := f.out
 /--
 error: Application type mismatch: In the application
   Foo.out' true
-the final argument
+the argument
   true
 has type
   Bool : Type

tests/lean/run/4888.lean

@@ -7,7 +7,7 @@ https://github.com/leanprover/lean4/issues/4888
 /--
 error: Application type mismatch: In the application
   Nat.succ True
-the final argument
+the argument
   True
 has type
   Prop : Type

tests/lean/run/DVec.lean

@@ -42,7 +42,7 @@ example (v : Vec Nat 1) : Nat :=
 /--
 error: Application type mismatch: In the application
   @DVec.hd ?_ v
-the final argument
+the argument
   v
 has type
   Vec Nat 1 : Type

tests/lean/run/check.lean

@@ -35,7 +35,7 @@ elab "elab_1eq1" : term => return expr_1eq1
 /--
 error: Application type mismatch: In the application
   @Eq Nat
-the final argument
+the argument
   Nat
 has type
   Type : Type 1
@@ -47,7 +47,7 @@ but is expected to have type
 /--
 error: Application type mismatch: In the application
   @Eq Nat
-the final argument
+the argument
   Nat
 has type
   Type : Type 1

tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean

@@ -2,9 +2,9 @@ def foo (x : Nat) (y : Bool) (z : Nat) (w : Nat) := ()
 /--
 error: Application type mismatch: In the application
   foo 1 true true
-the final argument
+the last
   true
-has type
+argument has type
   Bool : Type
 but is expected to have type
   Nat : Type

tests/lean/run/issue8213.lean

@@ -19,7 +19,7 @@ error: Failed to realize constant myTest.fun_cases:
     ⏎
       Application type mismatch: In the application
         motive mmotive x✝ h_1
-      the final argument
+      the argument
         h_1
       has type
         (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)

tests/lean/run/scopedunifhint.lean

@@ -30,7 +30,7 @@ def x : Nat := 10
 /--
 error: Application type mismatch: In the application
   mul ?_ x
-the final argument
+the argument
   x
 has type
   Nat : Type
@@ -43,7 +43,7 @@ but is expected to have type
 /--
 error: Application type mismatch: In the application
   mul ?_ (x, x)
-the final argument
+the argument
   (x, x)
 has type
   Nat × Nat : Type
@@ -58,7 +58,7 @@ local infix:65 (priority := high) "*" => mul
 /--
 error: Application type mismatch: In the application
   ?_*x
-the final argument
+the argument
   x
 has type
   Nat : Type
@@ -76,7 +76,7 @@ open Algebra -- activate unification hints
 /--
 error: Application type mismatch: In the application
   ?_*(x, x)
-the final argument
+the argument
   (x, x)
 has type
   Nat × Nat : Type
@@ -104,7 +104,7 @@ end Sec1
 /--
 error: Application type mismatch: In the application
   ?_*(x, x)
-the final argument
+the argument
   (x, x)
 has type
   Nat × Nat : Type

tests/lean/run/variable.lean

@@ -138,7 +138,7 @@ set_option pp.mvars false in
 /--
 error: Application type mismatch: In the application
   ToString True
-the final argument
+the argument
   True
 has type
   Prop : Type

tests/lean/simpArgTypeMismatch.lean.expected.out

@@ -1,6 +1,6 @@
 simpArgTypeMismatch.lean:3:29-3:33: error: Application type mismatch: In the application
   decide_eq_false Unit
-the final argument
+the argument
   Unit
 has type
   Type : Type 1

tests/lean/sorryAtError.lean.expected.out

@@ -1,6 +1,6 @@
 sorryAtError.lean:13:46-13:47: error: Application type mismatch: In the application
   ty.ty Γ
-the final argument
+the argument
   Γ
 has type
   x.ty.ctx : Type