It should be noted that soundness is not a common feature for type systems in the wild. It sounds kind of scary, "X programming language's type system is unsound", but that's pretty much been the status quo for most of programming.
I make analogies to taxonomy because before I learned software a biology teacher told me that taxonomy is also broken, so when I learned type theory it felt like a similar kind of broken.
We think putting wings to a mammal is adding behavior, when in fact it is subtracting it. Adding wings on a mammal means you have a bat, or a flying squirrel.
You have narrowed the potential of this type, not enhanced it. Anything else a mammal might do that bats can't? You've taken all of that away. Mammals with fly() aren't the fastest land animals. They don't have the record for holding their breath, or hibernation time. They can't dive(), speak() or useTool(). Really they're kinda useless except for vermin control.