OK. That sound reasonable. I think we should add the invariant "you never come back from a return expression so its type is Nothing." as a comment to `Types`.