Oh, it seems I've stumbled into a problem area. I skimmed the literature on this, and found that it is indeed a delicate question. Interestingly, the very question, how much coercions are different from subtypes, has already been discussed before:
Moreover, surprisingly, even my specific consideration has already been discussed. In the book "Funktionale Programmierung. Sprachdesign und Programmiertechnik" by Pepper and Hofstedt, in chapter seven, "Subtypen (Vererbung)", there is a relevant passage I want to quote, emphasis as in original:
Before we look at the individual constructions by which subtypes can be introduced and used, let us consider some general aspects.
Basically, what kinds of subtype formation one allows in a language is a design decision. How this decision is made has a massive impact on the expressive power of the language and on the complexity of the compiler. Even if – as for all design questions – the judgement cannot be made according to right/wrong, but rather according to criteria such as successful/corky or elegant/overloaded, there are nevertheless guidelines which one can orient oneself with the design. Of particular importance here is the context criterion.
Definition (Context Criterion)
The context criterion says: The subtype can occur everywhere where the supertype is expected. More precisely: Let S be a subtype of T. Then in every context c[. . .], in which elements of the type T are expected, elements of the subtype S can occur.
As we shall see, this criterion can help us whenever the "correct" definition of subtype is not immediately evident.
A second guideline is compatibility with the other typing aspects. The subtype relation should fit as "naturally" as possible into the world of type constructions. This has a particular effect on the relation to sum types.
As a consequence of this approach, we get an answer to an old controversial question: are subtypes (in the mathematical sense) true subsets or just subsets modulo a homomorphic embedding? In interaction with our other type constructions, the answer is: subtypes are subsets modulo homomorphic embedding.
Note: So as not to be misunderstood: This statement holds in the context of our general treatment of the typing idea. For languages that follow a different type philosophy, the answer may accordingly be different.