fix: let anonymous constructor notation elaborate with insufficient arguments (#10391)

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

@@ -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

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 } }

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⟩