From ede1acfb44a2251931cdbf689a119419ba75add7 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 15 Sep 2025 09:44:34 -0700
Subject: [PATCH] fix: let anonymous constructor notation elaborate with
 insufficient arguments (#10391)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR gives anonymous constructor notation (`⟨x,y⟩`) an error recovery
mechanism where if there are not enough arguments then synthetic sorries
are inserted for the missing arguments and an error is logged, rather
than outright failing.

Closes #9591.
---
 src/Lean/Elab/BuiltinNotation.lean | 11 +++++--
 tests/lean/1021.lean.expected.out  |  4 +--
 tests/lean/run/9591.lean           | 51 ++++++++++++++++++++++++++++++
 3 files changed, 62 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/9591.lean

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 73ebbd3a24..cf4129c237 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -70,15 +70,22 @@ open Meta
                 if (← getFVarLocalDecl xs[i]).binderInfo.isExplicit then
                   n := n + 1
               return n
-            let args := args.getElems
+            let mut args := args.getElems
             if args.size < numExplicitFields then
               let fieldsStr := if numExplicitFields == 1 then "fields" else "field"
               let providedStr :=
                 if args.size == 0 then "none were"
                 else if args.size == 1 then "only 1 was"
                 else s!"only {args.size} were"
-              throwError "Insufficient number of fields for `⟨...⟩` constructor: Constructor \
+              let errMsg := m!"Insufficient number of fields for `⟨...⟩` constructor: Constructor \
                 `{ctor}` has {numExplicitFields} explicit {fieldsStr}, but {providedStr} provided"
+              if (← read).errToSorry then
+                logError errMsg
+              else
+                throwError errMsg
+              for _ in args.size...numExplicitFields do
+                let s ← mkLabeledSorry (← mkFreshTypeMVar) (synthetic := true) (unique := false)
+                args := args.push <| ← exprToSyntax s
             let newStx ← if args.size == numExplicitFields then
               `($(mkCIdentFrom stx ctor (canonical := true)) $(args)*)
             else if numExplicitFields == 0 then
diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out
index 5dc8748974..1b3ac9ebdc 100644
--- a/tests/lean/1021.lean.expected.out
+++ b/tests/lean/1021.lean.expected.out
@@ -1,8 +1,8 @@
 some
   {
     range :=
-      { pos := { line := 210, column := 0 }, charUtf16 := 0, endPos := { line := 215, column := 31 },
+      { pos := { line := 217, column := 0 }, charUtf16 := 0, endPos := { line := 222, column := 31 },
         endCharUtf16 := 31 },
     selectionRange :=
-      { pos := { line := 210, column := 46 }, charUtf16 := 46, endPos := { line := 210, column := 58 },
+      { pos := { line := 217, column := 46 }, charUtf16 := 46, endPos := { line := 217, column := 58 },
         endCharUtf16 := 58 } }
diff --git a/tests/lean/run/9591.lean b/tests/lean/run/9591.lean
new file mode 100644
index 0000000000..319755fe8b
--- /dev/null
+++ b/tests/lean/run/9591.lean
@@ -0,0 +1,51 @@
+/-!
+# Error recovery for anonymous constructor notation
+https://github.com/leanprover/lean4/issues/9591
+
+When errToSorry is enabled, and too few arguments are provided, now it inserts `sorry`s
+while logging an error (rather than throwing an error).
+-/
+
+/--
+error: Insufficient number of fields for `⟨...⟩` constructor: Constructor `Prod.mk` has 2 explicit field, but none were provided
+---
+info: have this := (sorry, sorry);
+this : Nat × Nat
+-/
+#guard_msgs in #check show Nat × Nat from ⟨⟩
+
+/--
+error: Insufficient number of fields for `⟨...⟩` constructor: Constructor `Prod.mk` has 2 explicit field, but only 1 was provided
+---
+info: have this := (2, sorry);
+this : Nat × Nat
+-/
+#guard_msgs in #check show Nat × Nat from ⟨2⟩
+
+/--
+error: Insufficient number of fields for `⟨...⟩` constructor: Constructor `Prod.mk` has 2 explicit field, but only 1 was provided
+---
+error: Unknown constant `Nat.su`
+
+Note: Inferred this name from the expected resulting type of `.su`:
+  Nat
+---
+info: have this := (sorry, sorry);
+this : Nat × Nat
+-/
+#guard_msgs in #check show Nat × Nat from ⟨.su⟩
+
+/--
+info: have this := (2, 3);
+this : Nat × Nat
+-/
+#guard_msgs in #check show Nat × Nat from ⟨2,3⟩
+
+/-!
+The `first` tactic disables errToSorry, which is how the first `exact` throws an exception rather than logging an error.
+-/
+/--
+info: have this := (2, 3);
+this : Nat × Nat
+-/
+#guard_msgs in #check show Nat × Nat by first | exact ⟨1⟩ | exact ⟨2,3⟩