Why injection into sum type apparently leads to ambiguity?

Question

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?)

Answer 1

I think the key point here is $\sigma$, $\tau$ and $\phi$ are type variables, and not specific types. So, what the typing rule for $\operatorname{inl}$ says is that $\operatorname{inl} M$ is of type $\sigma + \tau$ for any $\tau$. The names of type variables don't matter, what matters is where else are you using the same type variable.