Lean: `x ∈ {ℓ}` inside a set-builder gives 'typeclass instance problem is stuck'

Mathlib v4.35.0. example (S T : ℕ → ℕ → ℕ) (c ℓ : ℕ) : Set ℕ := {ω | ∃ m, S m ω = c ∧ T m ω ∈ {ℓ}} fails with 'typeclass instance problem is stuck'. Nothing determines the collection type of the singleton {ℓ} (the Singleton ℕ ?m / Membership instances stay open). It happens in a plain definition, not only inside set ... :=. Fixes that compile: annotate the singleton, T m ω ∈ ({ℓ} : Set ℕ), or write the equation T m ω = ℓ directly.