timeout synthesizing MeasurableDiv2 R

Stream: mathlib4

[llllvvuu]

I was reminded of this again today: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/MeasurableDiv.20for.20Complex.20and.20Real.20types/near/419670355

I wrote it off at the time, but I wonder if the UX can/should be improved here? (if intended behavior, no problem, otherwise I'd be interested to learn how to fix this!)

In PNT+ I've put the following:

-- TODO: why do we need to bump this?
instance : MeasurableDiv₂ ℝ := by
  haveI (G : Type) [DivInvMonoid G] [MeasurableSpace G] [MeasurableInv G] [MeasurableMul₂ G] :
    MeasurableDiv₂ G := inferInstance
  exact this ℝ

[Mario Carneiro]

#mwe?

[llllvvuu]

The one from the linked message still works:

import Mathlib

instance : MeasurableDiv₂ ℂ := inferInstance
instance : MeasurableDiv₂ ℝ := inferInstance

https://live.lean-lang.org/#code=import%20Mathlib%0A%0Ainstance%20%3A%20MeasurableDiv%E2%82%82%20%E2%84%82%20%3A%3D%20inferInstance%0Ainstance%20%3A%20MeasurableDiv%E2%82%82%20%E2%84%9D%20%3A%3D%20inferInstance%0A

failed to synthesize
MeasurableDiv₂ ℂ
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached

I'm not well-versed in reading synthInstance traces but it looks like a maybe a wide search or a search that's getting stuck on non-true goals like DiscreteMeasurableSpace?