On Sat, Aug 8, 2020, 1:12 AM Steven D'Aprano 
Static languages often check what
bounds they can at compile time, and optionally insert bound checking runtime code for ambiguous places.

Yep. That's an assert, or it's moral equivalent.

Here's a deterministic program using the hypothetical new feature.

def plusone(i: int[1:1_000_000_000]):
    return i+1

random.seed(42)
for n in range(1_000_000):
      random.randint(1, 1_000_000_001)

Is this program type safe? Tell me by static analysis of Mersenne Twister.

Or if you want to special case the arguments to randint, will, lots of things. Let's say a "random" walk on the integer number line where each time through the loop increments or decrements some (deterministic but hard to calculate) amount. After N steps are we within certain bounds?