Lean timeouts after adding an instance

Stream: lean4

[Victor Porton]

After I changed a theorem to instance, lake build started to timeout. I didn't create a circular dependency by this instance. Here it is:

noncomputable def theorem515_completeSemilatticeSup
    [Filtrator.Primary α]
    [SemilatticeInf (Filtrator.subset (α := α))]
    [OrderTop α]
    [OrderBot α]
    (hcoreord :
      ∀ a b : Filtrator.subset (α := α),
        a.1 ≤ b.1 ↔
          @LE.le (Filtrator.subset (α := α))
            (inferInstance : SemilatticeInf (Filtrator.subset (α := α))).toPartialOrder.toLE
              a b) :
    CompleteSemilatticeSup (Filtrator.supset (α := α)) := by
    ...

noncomputable instance theorem515_completeLattice
    [Filtrator.Primary α]
    [SemilatticeInf (Filtrator.subset (α := α))]
    [OrderTop α]
    [OrderBot α]
    (hcoreord :
      ∀ a b : Filtrator.subset (α := α),
        a.1 ≤ b.1 ↔
          @LE.le (Filtrator.subset (α := α))
            (inferInstance : SemilatticeInf (Filtrator.subset (α := α))).toPartialOrder.toLE
              a b) :
    CompleteLattice (Filtrator.supset (α := α)) := by
  letI : CompleteSemilatticeSup (Filtrator.supset (α := α)) :=
    theorem515_completeSemilatticeSup (α := α) hcoreord
  exact completeLatticeOfCompleteSemilatticeSup (Filtrator.supset (α := α))

Any advice?

[Victor Porton]

Here is the code:

• https://github.com/vporton/atgt/blob/main/atgt/Filtrator/AdvancedProperties.lean
• https://github.com/vporton/atgt/blob/bug/instance-timeout/atgt/Filtrator/AdvancedProperties.lean

[Aaron Liu]

It is impossible for typeclass synthesis to fill in the hcoreord argument, so this should not be an instance.