From 995fa4766bff348aae006112feaaf680aa4acef0 Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Wed, 14 May 2025 12:12:10 -0400
Subject: [PATCH] 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                               |  9 ++++++++-
 tests/lean/243.lean.expected.out                       |  4 ++--
 tests/lean/283.lean.expected.out                       |  2 +-
 tests/lean/389.lean.expected.out                       |  2 +-
 tests/lean/423.lean.expected.out                       |  8 ++++----
 tests/lean/autoPPExplicit.lean.expected.out            |  2 +-
 tests/lean/doErrorMsg.lean.expected.out                |  2 +-
 tests/lean/doIssue.lean.expected.out                   |  2 +-
 tests/lean/elseifDoErrorPos.lean.expected.out          |  4 ++--
 tests/lean/evalSorry.lean.expected.out                 |  2 +-
 tests/lean/macroSwizzle.lean.expected.out              |  2 +-
 tests/lean/modBug.lean.expected.out                    |  2 +-
 tests/lean/motiveNotTypeCorect.lean.expected.out       |  2 +-
 tests/lean/nameArgErrorIssue.lean.expected.out         |  4 ++--
 tests/lean/namedHoles.lean.expected.out                |  4 ++--
 tests/lean/phashmap_inst_coherence.lean.expected.out   |  2 +-
 tests/lean/run/439.lean                                |  2 +-
 tests/lean/run/4405.lean                               |  2 +-
 tests/lean/run/4670.lean                               |  4 ++--
 tests/lean/run/4888.lean                               |  2 +-
 tests/lean/run/DVec.lean                               |  2 +-
 tests/lean/run/check.lean                              |  4 ++--
 .../run/duplicatedArgumentApplicationTypeMismatch.lean |  4 ++--
 tests/lean/run/issue8213.lean                          |  2 +-
 tests/lean/run/scopedunifhint.lean                     | 10 +++++-----
 tests/lean/run/variable.lean                           |  2 +-
 tests/lean/simpArgTypeMismatch.lean.expected.out       |  2 +-
 tests/lean/sorryAtError.lean.expected.out              |  2 +-
 28 files changed, 49 insertions(+), 42 deletions(-)

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index b5d11e986a..1ef9926127 100644
--- a/src/Lean/Meta/Check.lean
+++ b/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
diff --git a/tests/lean/243.lean.expected.out b/tests/lean/243.lean.expected.out
index 0950fe28cb..68c3dff208 100644
--- a/tests/lean/243.lean.expected.out
+++ b/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
diff --git a/tests/lean/283.lean.expected.out b/tests/lean/283.lean.expected.out
index 6edd141d8e..d8b534b351 100644
--- a/tests/lean/283.lean.expected.out
+++ b/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
diff --git a/tests/lean/389.lean.expected.out b/tests/lean/389.lean.expected.out
index fc9efe1015..11368e25f3 100644
--- a/tests/lean/389.lean.expected.out
+++ b/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
diff --git a/tests/lean/423.lean.expected.out b/tests/lean/423.lean.expected.out
index 0177652ad6..c40e75e03e 100644
--- a/tests/lean/423.lean.expected.out
+++ b/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
diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out
index 2960ed07de..42f0d7836f 100644
--- a/tests/lean/autoPPExplicit.lean.expected.out
+++ b/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
diff --git a/tests/lean/doErrorMsg.lean.expected.out b/tests/lean/doErrorMsg.lean.expected.out
index e218a20849..78835753d3 100644
--- a/tests/lean/doErrorMsg.lean.expected.out
+++ b/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
diff --git a/tests/lean/doIssue.lean.expected.out b/tests/lean/doIssue.lean.expected.out
index c474f90fcf..73cc58de9f 100644
--- a/tests/lean/doIssue.lean.expected.out
+++ b/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
diff --git a/tests/lean/elseifDoErrorPos.lean.expected.out b/tests/lean/elseifDoErrorPos.lean.expected.out
index 99a65bf8a3..c85affabed 100644
--- a/tests/lean/elseifDoErrorPos.lean.expected.out
+++ b/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
diff --git a/tests/lean/evalSorry.lean.expected.out b/tests/lean/evalSorry.lean.expected.out
index b03c41cf95..403b7e91d7 100644
--- a/tests/lean/evalSorry.lean.expected.out
+++ b/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
diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out
index dcf5aae0f0..64e2cd56c7 100644
--- a/tests/lean/macroSwizzle.lean.expected.out
+++ b/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
diff --git a/tests/lean/modBug.lean.expected.out b/tests/lean/modBug.lean.expected.out
index 97528d1899..59dc8d648c 100644
--- a/tests/lean/modBug.lean.expected.out
+++ b/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
diff --git a/tests/lean/motiveNotTypeCorect.lean.expected.out b/tests/lean/motiveNotTypeCorect.lean.expected.out
index d0006c70d7..17346b81c8 100644
--- a/tests/lean/motiveNotTypeCorect.lean.expected.out
+++ b/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
diff --git a/tests/lean/nameArgErrorIssue.lean.expected.out b/tests/lean/nameArgErrorIssue.lean.expected.out
index 648ee99b11..d8e8eabc97 100644
--- a/tests/lean/nameArgErrorIssue.lean.expected.out
+++ b/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
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index f1d0392bc7..4e3f66b468 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/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
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index 7b8952b48a..c07a90156a 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/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
diff --git a/tests/lean/run/439.lean b/tests/lean/run/439.lean
index 809aead580..fd3333876e 100644
--- a/tests/lean/run/439.lean
+++ b/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
diff --git a/tests/lean/run/4405.lean b/tests/lean/run/4405.lean
index cbe984b4a9..6178bba1f8 100644
--- a/tests/lean/run/4405.lean
+++ b/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
diff --git a/tests/lean/run/4670.lean b/tests/lean/run/4670.lean
index 6a457307eb..e78e788e9f 100644
--- a/tests/lean/run/4670.lean
+++ b/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
diff --git a/tests/lean/run/4888.lean b/tests/lean/run/4888.lean
index 08ea4f44c3..3a34394da7 100644
--- a/tests/lean/run/4888.lean
+++ b/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
diff --git a/tests/lean/run/DVec.lean b/tests/lean/run/DVec.lean
index 703df1cd75..fcc1a1673d 100644
--- a/tests/lean/run/DVec.lean
+++ b/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
diff --git a/tests/lean/run/check.lean b/tests/lean/run/check.lean
index bee9b835f9..8c9b58643e 100644
--- a/tests/lean/run/check.lean
+++ b/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
diff --git a/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean b/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean
index d1480e7447..af0b39f639 100644
--- a/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean
+++ b/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
diff --git a/tests/lean/run/issue8213.lean b/tests/lean/run/issue8213.lean
index 4579cce674..de42de10f7 100644
--- a/tests/lean/run/issue8213.lean
+++ b/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)
diff --git a/tests/lean/run/scopedunifhint.lean b/tests/lean/run/scopedunifhint.lean
index 79097242cf..72764c3200 100644
--- a/tests/lean/run/scopedunifhint.lean
+++ b/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
diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean
index dcfb521bab..233b10301f 100644
--- a/tests/lean/run/variable.lean
+++ b/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
diff --git a/tests/lean/simpArgTypeMismatch.lean.expected.out b/tests/lean/simpArgTypeMismatch.lean.expected.out
index 3dc3165fbc..883faffb77 100644
--- a/tests/lean/simpArgTypeMismatch.lean.expected.out
+++ b/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
diff --git a/tests/lean/sorryAtError.lean.expected.out b/tests/lean/sorryAtError.lean.expected.out
index 3963e4240e..30fcbce94f 100644
--- a/tests/lean/sorryAtError.lean.expected.out
+++ b/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