Why injection into sum type apparently leads to ambiguity?

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

• I think the 'Sums and Uniqueness of Types' section (p. 134) in the book contains several answers to this question. Apr 17 '16 at 17:35
• @Anton Trunov: I see, I ha dread several course notes and then started Pierce-s section on sums, but hadn't gotten that far. It's clear not that it is indeed ambiguous, and that there are ways to remove ambiguity. Thank you!
– josh
Apr 17 '16 at 17:55

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.
• This is a good observation, though it does mean you have to give up the notion that every term has one specific type. Most programming languages that deal with this parameterize inl in some way, effectively making separate inls for the different resulting sum types, though Scala does in fact do exactly what you suggest via variance.