Unhelpful error message on wrong `example` syntax

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When trying to supply a name to an example Lean complains in a way that does not help resolve the issue.

Steps to Reproduce

example foo: True := by trivial

Expected behavior: Lean tells me that examples can't have names.

Actual behavior: Lean prints the following unhelpful error message with foo highlighted

failed to infer binder type 
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) 
in the header are resolved before the declaration body is processed

Versions

Lean (version 4.0.0-nightly-2023-04-20, commit f9da1d8b55ca, Release)
Windows 11

Start by reproducing the reported example foo: True := by trivial case with the stated Lean version and compare the current diagnostic with the expected message. Trace the handling of named example declarations and update the behavior so this syntax reports that examples cannot have names; verify the resulting diagnostic with the reproduction.