coercion from subgroup to subset

Stream: Is there code for X?

[Kevin Buzzard]

A student just pointed out that this didn't work (and it's the sort of thing which sometimes didn't work in Lean 3 either):

import Mathlib

variable (G : Type) [Group G] [TopologicalSpace G] [TopologicalGroup G]

example (H : Subgroup G) : Prop := IsOpen H -- fails

example (H : Subgroup G) : Prop := IsOpen (H : Set _) -- fails

/-
typeclass instance problem is stuck, it is often due to metavariables
  TopologicalSpace (?m.455 H)
-/

example (H : Subgroup G) : Prop := IsOpen (H : Set G) -- works

I always feel like the first two should compile fine. Lean refuses to coerce from Subgroup G to Set G, presumably on the basis that there could in theory be some other coercion it's not found yet which goes from Subgroup G to Set Nat or whatever. Can we fix this with default coercions or some other mechanism in Lean 4?