I'll have to defer responding to the general idea of your latest post until later, but here's one quick quip:
```
IntTuple = Tuple[int, *Ts]
IntTuple # Behaves like Tuple[int, Any, ...]!?
```
I'm guessing there was a good reason that heterogeneous tuples of arbitrary length like this weren't supported by PEP 484?
I think we considered it as a future extension -- IIRC it's been proposed and we just didn't think there would be enough applications to warrant the extra complexity in mypy. I don't think there are particularly good theoretical reasons to reject it.