failed to synthesize reported at the beginning of a file

[adomani]

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

Sometimes, when the auto-filled in by infer_instance parameter fails to find an instance, it reports the error at the beginning of the file, instead of where the failure happened.

Context

Reported on the Lean Zulip.

Steps to Reproduce

Run this code:

  -- <-- `failed to synthesize A` here
class A

structure B where
  h1 : A := by infer_instance
-- using `inferInstance` instead of `by infer_instance` reports the
-- `failed to synthesize A` and the diagnostic comment here
-- not on the `example` below

example : B where

Expected behavior: The error should highlight example.

Actual behavior: The error highlights the beginning of the file.

Versions

[Output of #eval Lean.versionString]

"4.10.0-rc2"

for both the online server and my own computer.

[OS version, if not using live.lean-lang.org.]

Linux Mint

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

[kmill]

Could you clarify what you expect when it is := inferInstance? In that case, the error is on inferInstance, but that's because the original inferInstance fails to elaborate and the default value for B.h1 becomes sorry.

[adomani]

Looking again at this, I am not sure what I would expect with inferInstance. It seems that

class A

structure B where
  h1 : A := inferInstance

is already an error, so this is unrelated to the presence of the example. If default values such as this are not allowed, then the error is reported in the right place!

So, the only issue here, from my perspective, is the reporting of the error at the beginning of the file, rather that on example when the default value is set to by infer_instance.