Should the cast to ContinuousOpenMap be a `@[coe] def`?

Stream: mathlib4

[Anne Baanen]

While working on #8386, I spotted the following coercion in file#Mathlib/Topology/Hom/Open.lean:

instance [TopologicalSpace α] [TopologicalSpace β] [NDFunLike F α β]
    [ContinuousOpenMapClass F α β] :
    CoeTC F (α →CO β) :=
  ⟨fun f => ⟨f, map_open f⟩⟩

Should this not be a @[coe] def instead?

[Eric Wieser]

IMO this whole family of coercions is a simp-normal-form disaster, and having it unfold like that actually makes things better not worse

[Eric Wieser]

... but it also doesn't match the pattern we use for other types, so it would be justifiable to change it