Type system updates: moving from research into development

I guess the general description of the second example is that sometimes you can rule out certain return values of a function because they only occur under conditions that you already know will not be met in the given context.