Misleading extra "No goals to be solved" after unexpected type ascription

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

theorem foo : True := by
  let map_X_subset := fun (X': X.powerset) (o : Object) : Prop ↦
    sorry
  let Z := union (X.powerset.replace (P := map_X'_to_y) (by sorry))
  have X := 1

  sorry

This error message is misleading:

The actual problem is here:

Or at least I think so. I'm still learning the syntax.

The issue is that the big red squiggly line is much more noticeable and I did not notice the actual problem. So it would be nice to not show the misleading error message and to only show its upstream cause, assuming the two cases are possible to reliably disambiguate, or that it's fine to drop one of the error messages when you have two.

Context

Above

Steps to Reproduce

1. Above

Expected behavior: I'd expect to only see the type syntax error. I guess "no goals to be solved" would be OK to show in cases where it can reliably tell that in the presence of syntax errors, but in this case it looks like a false positive.

Actual behavior: Both errors are shown, including "no goals to be solved" (which is kind of not true in my example).

Versions

nightly from the website

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

No source file or test is named. Start by running the minimal reproduction against the Lean nightly release and compare the two reported diagnostics; done means the misleading "No goals to be solved" message is omitted when the upstream type syntax error makes it a false positive.