Error message at the start of file

Stream: mathlib4

[Gareth Ma]

Compiling the following code, the error message shows up at the start of the file

import Mathlib.Topology.Order
import Mathlib.Algebra.Module.Zlattice.Basic

structure A where
  S : AddSubgroup ℝ
  S_discrete : DiscreteTopology S := by infer_instance
  S_lattice : IsZlattice ℝ S := by infer_instance

def T := AddSubgroup.zmultiples (1 : ℝ)
theorem aux : Submodule.span ℝ (T : Set ℝ) = ⊤ := by
  ext x
  simp [T]
  apply Set.mem_of_subset_of_mem (s₁ := Ideal.span ({1} : Set ℝ))
  · apply Ideal.span_mono
    simp
  · simp

def B : A where
  S := T
  S_lattice := by
    -- constructor
    use aux

(verified on the online Lean 4 playground) That seems like a bug to me. constructor correctly(?) errors on the spot

[Gareth Ma]

import Mathlib.Topology.Order
import Mathlib.Algebra.Module.Zlattice.Basic

class Inst1
class Inst2 extends Inst1
structure A where
  h1 : Inst1 := by infer_instance
  h2 : Inst2 := by infer_instance

axiom inst2 : Inst2
noncomputable def B : A where
  h2 := inst2

Not sure if this is a proper minimisation but it has the same problem

[Gareth Ma]

I don't have permissions to move this across channels but maybe this belongs in #lean4

[Damiano Testa]

This one is mathlib-free and slightly shorter: the error appears to be reported starting from the first character of the file.

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

[Marc Huisinga]

Damiano Testa said:

This one is mathlib-free and slightly shorter: the error appears to be reported starting from the first character of the file.

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

Could you report this issue in the Lean 4 repository?

[Damiano Testa]

Done #4880