> 1. Some edge case seems to be that if *tuple[...] is involved on either side we will never simplify. Or perhaps a better rule is that *tuple[...] is never simplified away (but fixed items before and after it may be).

I do not understand this. Do you forbid simplifying of tuple[*Ts, float][str, *tuple[int, ...]] to tuple[str, *tuple[int, ...], float]?

I think that the rule should be that *tuple[X, ...] cannot split between different variables. Or that it cannot substitute a TypeVar. A more strong variant of rule 4.

> 5. ... but we cannot flag it as an error either.

I think that it will better to flag it as an error now. Later, after all code be merged and all edge cases be handled we can return here and reconsider this.

There are workarounds for this.

* You should not use Generic[*Ts] if you require at least one item, but Generic[*Ts, T].
* Instead of `def foo(*args: *Ts)` use `def foo(*args: *tuple[*Ts, T])`.

These tricks are common in functional programming.

The rest of the rules match my implementations more or less.