feat: guard against synthetic sorry misuse

src/Lean/Log.lean

@@ -60,7 +60,10 @@ We use the `fileMap` to find the line and column numbers for the error message.
 -/
 def logAt (ref : Syntax) (msgData : MessageData)
     (severity : MessageSeverity := MessageSeverity.error) (isSilent : Bool := false) : m Unit :=
-  unless severity == .error && msgData.hasSyntheticSorry do
+  -- Filter out follow-up errors on synthetic sorries, which should only be created when an error
+  -- for the relevant part of the input has already been logged. However, in case this invariant
+  -- was accidentally broken and no error has been logged yet, log at least one error.
+  unless severity == .error && msgData.hasSyntheticSorry && (← MonadLog.hasErrors) do
     let severity := if severity == .warning && warningAsError.get (← getOptions) then .error else severity
     let ref    := replaceRef ref (← MonadLog.getRef)
     let pos    := ref.getPos?.getD 0

tests/lean/doLetLoop.lean.expected.out

@@ -1,2 +1,5 @@
 doLetLoop.lean:4:0: error: unexpected end of input
-doLetLoop.lean:2:4-2:5: warning: declaration uses 'sorry'
+doLetLoop.lean:3:2-3:8: error: failed to synthesize
+  Decidable sorry
+
+Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/doSeqRightIssue.lean.expected.out

@@ -1,3 +1,7 @@
 doSeqRightIssue.lean:5:23-5:24: error: unknown universe level 'v'
-doSeqRightIssue.lean:8:0-9:40: warning: declaration uses 'sorry'
-doSeqRightIssue.lean:7:8-7:10: warning: declaration uses 'sorry'
+doSeqRightIssue.lean:7:36-7:39: error: type mismatch
+  β a
+has type
+  sorry : Sort ?u
+but is expected to have type
+  Type ?u : Type (?u + 1)

tests/lean/run/2226.lean

@@ -6,7 +6,14 @@ A : Nat
 #guard_msgs in
 variable (A : Nat) (B : by skip)
 
-/-- error: failed to infer definition type -/
+/--
+error: type mismatch
+  B
+has type
+  sorry : Sort ?u.9
+but is expected to have type
+  Nat : Type
+-/
 #guard_msgs in
 def foo :=
   A = B

tests/lean/run/3214.lean

@@ -11,4 +11,15 @@ term has type
 #guard_msgs in
 variable {α : Type} (s : Missing α)
 
+/--
+error: application type mismatch
+  Foo s
+argument
+  s
+has type
+  sorry : Sort _
+but is expected to have type
+  Type : Type 1
+-/
+#guard_msgs in
 #synth Foo s

tests/lean/silent_failure.lean

@@ -0,0 +1,7 @@
+-- Prior to https://github.com/leanprover/lean4/pull/8230
+-- this  failing silently (but not adding `g` to the environment).
+
+#guard_msgs (drop info) in
+partial def g :
+  have : False := by apply?
+  False := g

tests/lean/silent_failure.lean.expected.out

@@ -0,0 +1,3 @@
+silent_failure.lean:5:12-5:13: error: invalid use of 'partial', 'g' is not a function
+  let_fun this := ⋯;
+  False