By subtyping, here I mean implicit coercion between types, not sig.
In programming languages, sum types have associated data and it matters which variant is being used, so e.g. A can not be a subtype of Either<A,B> in haskell. The same is true for decideable coq. That is, A can not be a subtype of A + B in general, since A + A has one bit more data than A.
However, Props have no data in runtime, so why coq doesn't consider A a subtype of A \/ B and allow using each member of it as a member of A \/ B without explicit or_introl? I think it makes proof shorter and more generic. Is there a fundamental limit or unsoundness problem that makes it impossible, or it is just an unneeded feature?
I think the main issue is indeed one of utility:
If you're looking at proving A\/B, you probably aren't building a proof of A or B by hand, but rather applying a bunch of powerful techniques with no regard for efficiency or conciseness, for exactly the reasons you said.
This means you can apply powerful tactics such as auto or intuition, or even firstorder if you're feeling lucky.
These tactics prove much more than A -> A \/ B, and often perform many steps, including that one, which makes the coercion somewhat useless (and perhaps even confusing!).