I have been reading Benjamin Pierce's Types and Programming Languages, plus a couple of course notes on type systems and typed $\lambda$-calculus, and there is one thing I don't get: it seems that everybody defines sum types in the same way, and they way the language is extended to accommodate this new type includes the following typing rules:
- if $\sigma$ and $\tau$ are types, then $\sigma+\tau$ is a type
- if $M$ is of type $\sigma$, then $\operatorname{inl} M$ is of type $\sigma+\tau$
- symmetrically for $\operatorname{inr}$, if $M$ is of type $\tau$, then $\operatorname{inr} M$ is of type $\sigma+\tau$.
However, suppose I have two sum types, $\sigma+\tau$ and $\sigma+\phi$, and also that $M$ is of type $\sigma$. Then it is not clear what the type of $\operatorname{inl} M$ is.
Is there something I missed, or is this really how sum types work? Because it would be quite easy to actually "fix" the definition to allow one to immediately infer the type of $\operatorname{inl} M$ in the example above -- just include the sum type in the annotation:
$\operatorname{inl_{\sigma+\tau}} M$ is, of course, of type $\sigma+\tau$.
But this is not what is usually done. Why? (Or is it actually done, implicitly?)