Consider that a valid inference for this
simple(2, 3)
is that _T is Literal[2, 3]
x is Literal[2] and y is Literal[3] and that could look like x and y are not the same type.
Would it be possible to mandate a minimum number of constraints a compliant constraint solver must attempt to solve and a minimum amount of context it should attempt to use without fully specifying constraint solving right now to get a baseline that is reliable for the typeshed? I’ve seen your argument for not allowing an infinite number of them with language server responsiveness before, and understand the concerns are different for different type checkers, but it seems like the primary issue at hand is that the typeshed needs to know what it can and cannot use in stubs.