SubspaceTopology Coercion

[Columbus240]

Is it possible (and easy to use) to create a coercion from Ensemble X to TopologicalSpace via @SubspaceTopology X, where X : TopologicalSpace?
This would be useful, because it allows some things to be stated more concisely (and is often done in mathematical practice). For example the notions "compact subset" or "connected subset" of a space would be automatically clear and wouldn't need to be defined separately.

The code

Coercion SubspaceTopology : Ensemble >-> TopologicalSpace.

Produces the warning SubspaceTopology does not respect the uniform inheritance condition [uniform-inheritance,typechecker] and Coq still says that SubspaceTopology is now a coercion.
But still, the following does not work:

From Topology Require Import SubspaceTopology Connectedness.
Coercion SubspaceTopology : Ensemble >-> TopologicalSpace.
Section S.
  Variable X : TopologicalSpace.
  Variable U : Ensemble X.
  Fail Variable V : Ensemble U.
  Fail Variable p : U.
  Fail Variable f : U -> X.
  Fail Goal connected U.
End Section S.

These basics would be necessary to simplify work with subspaces.