As I mentioned in another related thread, it is possible to write an implementation of a TypeIs function that subverts the rules of the type system. There are not-so-subtle ways to get it wrong (such as unconditionally returning True), and there are more subtle ways. This thread contains some good examples of implementations that are subtly wrong from a soundness perspective.
I can speak from personal experience (having implemented the type guard functionality in pyright) that it’s difficult to get type narrowing logic correct in all cases. There are many conditions to consider, and the rules can be abstruse. Even in cases where the rules are well established and clear, there are tradeoffs between usability and soundness that must be considered.
From my perspective, the implementation of the TypeIs function in Mike’s clever example subverts the rules of the type system and therefore introduces unsoundness. Given the (carefully crafted) conditions of this example, one cannot determine whether a value of type A[int | str] can be safely narrowed to an A[int] simply by doing an isinstance check of a.i. This check could preserve soundness if one were to either: 1) mark A as @final, or 2) modify the value constraints for X so they are non-overlapping.
If your goal in writing this TypeIs function is not full soundness but rather some balance between soundness and usability, then it’s a fine implementation and will probably serve you well. This depends on your use case and goals. If you’re a stickler for type soundness, then this implementation is problematic, as Mike has demonstrated.
One can think of the TypeIs mechanism (and the TypeGuard mechanism that preceded it) as a way to extend the functionality of a type checker. It’s somewhat akin to mypy’s plugin mechanism but more constrained and standardized. Just as it’s possible to write a mypy plugin that subverts the rules of the type system, it’s possible to write a TypeIs function that does so. That doesn’t mean TypeIs should be thrown out. (Nor should mypy’s plugin mechanism.) TypeIs is important and useful because type checkers provide built-in support for only a limited number of expression forms. If your needs go beyond the built-in capabilities of your type checker, TypeIs provides a way to handle additional use cases. It is a tool that can be used (or abused) as you see fit.
Jelle wrote a guide that helps users avoid some common mistakes with TypeIs. This guide could be extended if we want to document additional considerations, but I’ll note that it already goes well beyond any guidance I’ve seen in the TypeScript world on this topic. (In fact, the example provided in the official TypeScript guide is demonstrably unsound. Edit: actually, it is sound because they’re making a copy of the array.) In the Python world, I feel pretty good about the guidance we have in place now.