As part of building up constraint sets, we produce a "sequent map" (aka a Horn clause database) describing how all of the individual constraints in the constraint set, and any derived constraints, relate to each other. Part of this is building up transitive relationships. For instance, if we know that S ≤ int and int ≤ T, we can infer that S ≤ T.

In astral-sh/ruff#22411, we started seeing some false positive diagnostics, whose root cause seems to be sequents of the form S ≤ Any ∧ Any ≤ T → S ≤ T. That is, exactly the same as above, but with Any as the "pivot" instead of int. But that's not valid, since there's no guarantee that the two Anys will materialize to the same type. In other words, we should be performing a subtyping check during sequent map constructing, not an assignability check.