Specs clarification: `TypeIs` works with all types, structural or nominal

Typing
1

Currently, this is how Pyright behaves towards a TypeIs[Callable[..., ...]] narrowing function, which is rather confusing:

def function_expects_no_arguments(fn: Callable[..., Any]) -> TypeIs[Callable[[], Any]]: ...

def f[**P](fn: Callable[[], None] | Callable[P, None]) -> None | Callable[P, None]:
    if function_expects_no_arguments(fn):
        reveal_type(fn)  # Revealed: (() -> None) | ((**P@f) -> None)
                         # Should be: () -> None
    else:
        reveal_type(fn)  # Revealed: () -> None
                         # Should be: (**P@f) -> None

(As an aside, type checkers treat it very differently; playgrounds: Pyright, Mypy, Pyrefly.)

@erictraut argues that:

TypeIs is designed to use isinstance (inheritance) semantics for type narrowing. Callable is a structural type, and the spec is not clear what the behavior should be in this case.

The specification says:

As a rule of thumb, a type checker should use the same type narrowing logic ā€“ and get results that are consistent with ā€“ its handling of isinstance().

However, I would say TypeIs should work equally fine with all types, structural or nominal. I propose that this requirement be added to the spec.

2 Likes
2

The less rule of thumb bit right before the part of the specification you quoted is:

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. Type checkers should fall back on practical approximations of these types.

I think including TypeIs prior to Intersections was a mistake and said as much at the time, but you may need to wait for Intersection work to be finished to be able to expect consistent behavior across typecheckers here given that the formal definition relies on them, but then kicks that down the curb and says ā€œuse an approximationā€

Using the current draft of intersections, this would work as you seem to expect.

1 Like
3

(After some discussion out of band)

TypeIs may not be what you want here. Using TypeGuard should work for the positive branch today.

Thereā€™s a problem with using intersections to narrow here because there is a type that is ā€œmore compatibleā€ than your intent. Intersecting a gradual callable with a structural type that accepts no parameters in that you havenā€™t ruled out that it can also take parameters.

A function like:

def x(foo: int = 0, /) -> None:  ...

Is compatible with the structural type Callable[[], None] and Callable[..., Any]

1 Like
4

Could you link what youā€™re referring to?

5

You can find the latest draft here, along with some discussion of what still is missing from it: [RFC] Latest status of draft Ā· Issue #53 Ā· CarliJoy/intersection_examples Ā· GitHub

The tough questions around Any have answers already, so most of what is left is writing up examples, specifically showing what this solves, how it interacts with other ā€œspecialā€ parts of the type system such as with dataclass_transform, and some language changes around TypeIs and Never.

As TypeIs is basically a limited Intersection already and specified as such, any improvement in the specification of the expectations of intersections, including adding them directly, will improve usability of TypeIs.

1 Like