Why is this function type-correct