A typevar should specialize to a single type each time its generic class or function is specialized. We're already considering that, and have a (currently failing) mdtest for this example:

def f[T: (int, str)](t: T, u: T) -> T:
  return t + u

This is valid since int has an __add__ method that takes in another int, and str has one that takes in another str. It's not an error that int's method doesn't take in a str, since if t is an int, u must be one too. This is an important way that constrained typevars are different from a union.

@carljm and I were trying to brainstorm whether this kind of propagation could occur across multiple statements, and he came up with this example:

def f[T](a: T, b: T):
    if isinstance(a, int):
        reveal_type(a)  # revealed: int
        reveal_type(b)  # hopefully: int

The narrowing constraint machinery seems like it provides what we need to make this work — the isinstance call would (waving hands wildly) not just add a narrowing constraint on a, but also on any typevars that appear in the type of a.