Moreover the immutability isn't necessary. The problem at-hand arose from forming a shared interface for the trait NatPos because we don't have first-class intersections with tagged instances. Afair, the research paper was assuming that the types were untagged and thus we could write to an instance as a Nat and read from it as Pos. Tagging forces de-structuring that disallows doing that.
My real motivation has been first-class intersections and unions as I think they will be necessary for composability, but I will want to discuss that in a different thread.