It is obvious (to us) that everything after the return statement can be considered the else branch of the if, and so smart casting should behave identically to how it would behave if there was an actual else branch.