TypeIs narrowing for certain parameterized containers doesn't make sense

[Sachaa-Thanasius]

Describe the bug
When using TypeIs with a guard function that's meant to narrow the parameterized type of some types of containers, the type pyright infers when that function is used doesn't make sense. I didn't narrow down which containers this occurs with, but gave two as an example below.

Code or Screenshots

from typing import MutableSequence
from typing_extensions import TypeIs, reveal_type

# ==== 1) With a list:

def _is_list_of_str(lst: list[str | tuple[str, object]]) -> TypeIs[list[str]]:
    """A relatively weak heuristic to narrow the type of the list to list[str]."""

    return isinstance(lst[0], str)


def example1(thing: list[str | tuple[str, object]]):
    if _is_list_of_str(thing):
        reveal_type(thing)  # Type of "thing" is "<subclass of list and list>"
        # This result doesn't make sense to me. Expected "list[str]".
    else:
        reveal_type(thing)  # Type of "thing" is "list[str | tuple[str, object]]"
        # This doesn't take into account that list[str] would be eliminated as a possibility in this branch. Expected "list[tuple[str, object]]".


# ==== 2) With a MutableSequence:

def _is_mut_sequence_of_str(
    seq: MutableSequence[str | tuple[str, object]],
) -> TypeIs[MutableSequence[str]]:
    return isinstance(seq[0], str)


def example2(thing2: MutableSequence[str | tuple[str, object]]):
    if _is_mut_sequence_of_str(thing2):
        reveal_type(thing2)  # Type of "thing2" is "<subclass of MutableSequence and MutableSequence>"
        # Again, doesn't make sense to me. Expected "MutableSequence[str]".
    else:
        reveal_type(thing2)  # Type of "thing2" is "MutableSequence[str | tuple[str, object]]"
        # Again, doesn't take into account narrowing from being in this branch. Expected "MutableSequence[tuple[str, object]]".

VS Code extension or command-line
This was replicated in VSCode via Pylance, version 2024.6.1.

[erictraut]

These are invalid uses of TypeIs. The TypeIs form requires that the narrowed type is a subtype of the pre-narrowed type. In both of your examples, this condition isn't met. The type list[str] is not a subtype of list[str | tuple[str, object]].

If you enable basic type checking diagnostics, you will observe that pyright displays errors about your usage of TypeIs.

The TypeGuard form allows you to specify a narrowed type that is not a subtype of the pre-narrowed type, but this is technically unsafe from a type perspective.

In any case, this is not a bug in pyright, so I'm closing the issue.

[Sachaa-Thanasius]

Interesting. I feel like this behavior is disputable, but if I choose to pursue that, it'll be later. For now, I'll just note that I set pyright on strict mode, but Pylance didn't actually point out that this TypeIs usage is invalid. I'll see if there's a bug in my setup.

EDIT: Turns out there was a rogue configuration file with reportGeneralTypeIssues set to "none". Plain ol' user error.

[mikeshardmind]

Edit: Post left mostly as is for posterity, can be ignored, I made a mistake when considering this see very bottom of post or followup

The TypeIs form requires that the narrowed type is a subtype of the pre-narrowed type. In both of your examples, this condition isn't met.

This requirement isn't expressed in the pep for it, the actual requirement which was accepted specified it in terms of consistency:

The return type R must be consistent with I. The type checker should emit an error if this condition is not met.

The term "consistent with" is not extremely well defined, but the above usage meets the requirement of this for what most people would expect, and this matches the ongoing work in the PR python/typing#1743

The latter language indicating set-theoretic definitions, while not firmly in the specification at this point in time, would match this interpretation for what the behavior should be (also quoted below). This seems to support the interpretation that this should be an allowed use.

The resulting narrowing in the positive case and the negative case are also well specified, but the negative narrowing might have surprising behavior to some here, as the negative would still include the non-homogenous original form.

Formally, type NP should be narrowed to A∧R, the intersection of A and R, and type NN should be narrowed to A∧¬R, the intersection of A and the complement of R. In practice, the theoretic types for strict type guards cannot be expressed precisely in the Python type system.

Taking the original examples

def _is_list_of_str(lst: list[str | tuple[str, object]]) -> TypeIs[list[str]]:
    ...  # I've left out the original implementation, 
    # as the implementation was unsafe for what was expressed.
    # however, the pep also does not say that it's an error for someone to write an unsafe typeis

def example1(thing: list[str | tuple[str, object]]):
    if _is_list_of_str(thing):
        # list[str]
    else:
        #  list[str | tuple[str, object]] & ~list[str]
        # notably, this could still include `str` elements

This becomes more obvious when considering that all of the below are consistent with list[A | B], including the non-denotable forms. (Edit: No, these aren't consistent with as types. As values having that exact type, they could be, variance failure on my part)

• list[A]
• list[B]
• list[A | B] & ~list[A]
• list[A | B] & ~ list[B]
• list[A | B] & ~list[A] & ~list[B]
• list[A | B]

[DiscordLiz]

Neither the consistency nor the subtyping rule would actually be type safe. I think the consistency rule is correct, and this falls under users writing potentially unsafe TypeIs functions and that TYpeIs would be unsafe in concurrent access situations.

Here's an example that type checks fine by using sequence, but will error at runtime.

Code sample in pyright playground

import asyncio
from typing import Sequence
from typing_extensions import TypeIs

class A:  pass
class B(A):
    def __init__(self, use_count: int = 0):
        self.use_count = use_count

def is_seq_b(x: Sequence) -> TypeIs[Sequence[B]]:
    return all(isinstance(i, B) for i in x)

async def takes_seq(x: Sequence[A]):
    if is_seq_b(x):
        await asyncio.sleep(10)
        users = sum(i.use_count for i in x)

async def takes_list(x: list[A]):
    t = asyncio.create_task(takes_seq(x))
    await asyncio.sleep(1)
    x.append(A())
    await t

if __name__ == "__main__":
    lst: list[A] = [B(i) for i in range(10)]
    asyncio.run(takes_list(lst))