bug in `@[derive]`?

Stream: general

[Kevin Buzzard]

Lean 3 (yeah I know Lean 3 is so early 2022, but I'm trying to get some PRs off the review queue before a possible flag day):

import topology.instances.real

example : topological_ring ℝ := infer_instance -- works
example : topological_space ℝ := infer_instance -- works

@[derive topological_ring]
def my_reals := ℝ
/-
failed to synthesize type class instance for
⊢ topological_space my_reals
-/

Should that not be happening?