Couldn't you have a constraining operation in there to assert that you have enough bits? You are right that we don't know if `a + b` would need more bits than

Couldn't you have a constraining operation in there to assert that you have enough bits? You are right that we don't know if `a + b` would need more bits than either a or b. However, we could have an assert that allows us to ensure the static constraints are satisfied. And the type system could be used as a place to know where we haven't checked the constraint. (Note that I'm not too clear how valuable this would be. Just asking why that isn't a valid path.)