can't infer `ContinuousNeg`

Stream: mathlib4

[Jireh Loreaux]

Here's a neat trick, and note that etaExperiment doesn't help. Any ideas?

import Mathlib.Topology.Algebra.Group.Basic
-- import Mathlib.Topology.Algebra.Ring.Basic

example [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] : ContinuousAdd β :=
  inferInstance -- works
example [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] : ContinuousNeg β :=
  inferInstance -- works, but times out if you add the import above, and that import seems to be minimal to reproduce
example [TopologicalSpace β] [AddGroup β] [TopologicalAddGroup β] : ContinuousNeg β :=
  TopologicalAddGroup.toContinuousNeg -- works

[Floris van Doorn]

It seems to try to find NonUnitalNonAssocRing β over and over again:

[Meta.synthInstance] 💥 ContinuousNeg β ▼
  [] new goal ContinuousNeg β ▶
  [] ❌ apply @TopologicalRing.toContinuousNeg to ContinuousNeg β ▼
    [tryResolve] ❌ ContinuousNeg β ≟ ContinuousNeg ?m.1596 ▼
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
      [] ❌ NonUnitalNonAssocRing β ▶
[...]

Is this a previously noticed bug in type class inference?

[Matthew Ballard]

lean4#2055

[Matthew Ballard]

Happening over at #mathlib4 > !4#2797 / !4#2769 also

[Jireh Loreaux]

Yes, I just asked Gabriel about it during the meeting and it's a known issue, as Matthew linked.