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, Prop
s 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?