subtype: Tweak the diagonal rule to make it more clear (#61861)

Pop quiz: Which of these make `T` diagonal:

```
Tuple{S, T} where S<:T where T
Tuple{S, T} where S<:Tuple{T} where T
Tuple{S, T} where S<:Tuple{T,T} where T
```

The answer right now is 2 and 3, but I would argue that 2 is a bit of an
accident of implementation, because `Tuple` turns back on the variable
occurrence counting that the typevar consitency check tried to turn off
(but we depend on `3` and it clearly "looks" diagonal).

This PR changes the semantics so that 2 is no longer considered
diagonal. Instead, the diagonal rule conceptually applies to `Tuple`s:
The diagonal rule applies whenever any `Tuple` sees 2+ active typevars
in covariant position (and the typevar was not statically found in
invariant position by the outer UnionAll - same as before).

For a more extensive set of examples of cases that change behaviors, see
the test suite, but of note none of our existing tests depended on this
(other than a test_broken that now passes).

A particular motivation for this change is intersection, since
intersection needs to extensively reason about whether or not it is
possible for a variable to become diagonal (no intersection changes are
made in this PR, because intersection is not currently correct with
respect to various diagonal cases - however fixing that requires
defining what correctness means).

Idea by me. Tests by GPT-5.5 Pro. Implemented by Claude Opus 4.7.