Coming back to this now, I realize there is no way that we could have subsumption with Rust's trait objects because NatPos does not implement Nat and Pos separately, because a trait can't implement a trait (which is essentially equivalent to @troiganto's comment).
I was rushing when I wrote down that code, and on reflection obviously a trait object NatPos can't be cast to an implementaion of struct Unsigned for traits Nat or Pos, because the Rust compiler does not know which implementation of NatPos the reference points to (this is only known at runtime for the trait objects dictionary).
Such can only be possible if Nat and Pos are classes in an OOP language (or traits in Scala) which can contain their own implementation. Perhaps it is my familiarity with Scala and its apparent conflation of trait with classes (in a subclassing model that linearizes trait implementations) that may have caused my mental mode to be incorrect about expectation for traits in Rust. I do note that Rust has default methods for traits though, so in theory Nat and Pos could have their own implementations (which may have been another factor that caused me to conflate them with Scala traits semantics), but nevertheless Rust doesn't allow casting a trait object from NatPos to either Nat or Pos.
So I think I can now answer my own question #1 by concluding that subclassing languages (C++, Java, Scala, etc) appear to have this problem that I outlined and it is a well known as the Circle-Ellipse (aka Square-Rectangle) violation of the Liskov Substitution Principle (LSP) due to mutable references and subsumption elimination. Subsumption elimination occurs when casting or assigning (i.e. coercing) NatPos to one of its base types in a subclassing language. The Circle-Ellipse problem is due to the ability to mutate a Circle with the Ellipse's interface.
What do we do when we have a NatPos trait object and a function requires a Pos or a Nat trait object input?
If we implement our data type on both Nat and Pos, then if we have a reference to one, we can't cast it to a reference to the other. That is good because it avoids the bug where Nat has a value of 0 as I explained upthread. But consider Read and ReadWrite traits instead of Nat and Pos. If we have a ReadWrite trait object, we can't call a function that expects a Read trait object. This is the motivation for intersections, so that Read and ReadWrite are subtypes of Read /\ Write.
Robert Harper wrote:
There are two fundamental problems with type classes. The first is that they insist that a type can implement a type class in exactly one way. For example, according to the philosophy of type classes, the integers can be ordered in precisely one way (the usual ordering), but obviously there are many orderings (say, by divisibility) of interest. The second is that they confound two separate issues: specifying how a type implements a type class and specifying when such a specification should be used during type inference. As a consequence, using type classes is, in Greg Morrisett’s term, like steering the Queen Mary: you have to get this hulking mass pointed in the right direction so that the inference mechanism resolves things the way you want it to.
Reactions to Robert Harper's points.
Thus subtyping with intersections appear to be necessary for functional composition, but they open the Pandora's box to the problem I have explained. I am curious to hear if anyone has a solution that provides both composition and avoids the problem of violations of LSP that I have explained?
The only solution I currently envision is immutable references (Copy types could still be mutable) combined with subtyping and intersections. Then I want to consider making the dictionaries for the trait objects orthogonal to the objects, so that it is possible to track data types at compile-time and supply the dictionaries as a separate inputs to the function, which I think may be a complete solution to the Expression Problem (but I may also be mistaken). This is the new thread I was contemplating to write, but I am also trying to better understand other strategies that have been mentioned such as OOHaskell.
I am incorporating what I want to respond on that thread into my statements above.
Although I didn't really digest all that discussion, that appears to be the reversal of the relationship between covariance and contravariance (given by the LSP) given by relative direction of inheritance for the nominal type and the methods of the nominal type. This reversal occurs again for each parameter of a method and again for each parameter of a parameter, etc..