Calling a function that expects `T | Sequence[T]`. (typecheckers diverge)

Typing
1

I noticed some severe divergences between different type checkers when calling a generic function that expects T | Sequence[T][1]. The problems arise when we feed in a type that is simultaneously a subtype of T and of Sequence[T], indicating that the expected behavior is currently underspecificied.

# fmt: off
from collections.abc import Sequence
from typing import reveal_type as r


class Foo: ...
class Seq[F: Foo](Sequence[F], Foo): ...

def concat[L: Foo, R: Foo](
    left: L | Sequence[L],   # actually want `L | (Sequence[L] & ¬L)`
    right: R | Sequence[R],  # actually want `R | (Sequence[R] & ¬R)`
) -> list[L | R]:
    return []

def test[F1: Foo, F2: Foo](
    f1: F1, l1: list[F1], s1: Seq[F1],
    f2: F2, l2: list[F2], s2: Seq[F2],
) -> None:
    # results            mypy            pyright         pyrefly         ty
    # foo + foo
    r(concat(f1, f1))  # list[F1]        list[F1]        list[F1]        e:arg-type
    r(concat(f1, f2))  # list[F1 | F2]   list[F1 | F2]   list[F1 | F2]   e:arg-type
    # list + list
    r(concat(l1, l1))  # list[F1]        list[F1]        list[F1]        list[list[F1]]
    r(concat(l1, l2))  # list[F1 | F2]   list[F1 | F2]   list[F1 | F2]   list[list[F1] | list[F2]]
    # seq + seq
    r(concat(s1, s1))  # e:arg-type      list[F1]        list[F1]        list[Seq[F1]]
    r(concat(s1, s2))  # e:arg-type      list[F1 | F2]   list[F1 | F2]   list[Seq[F1] | Seq[F2]]
    # foo + list
    r(concat(f1, l1))  # list[F1]        list[F1]        list[F1]        e:arg-type
    r(concat(f1, l2))  # list[F1 | F2]   list[F1 | F2]   list[F1 | F2]   e:arg-type
    # foo + seq
    r(concat(f1, s1))  # e:arg-type      list[F1]        list[F1]        e:arg-type
    r(concat(f1, s2))  # e:arg-type      list[F1 | F2]   list[F1 | F2]   e:arg-type
    # list + seq
    r(concat(l1, s1))  # e:arg-type      list[F1]        list[F1]        list[Seq[F1] | list[F1]]
    r(concat(l1, s2))  # e:arg-type      list[F1 | F2]   list[F1 | F2]   list[Seq[F1] | list[F2]]

Take the case concat(Seq[F1], Seq[F1]). So we first need to check and bind Seq[F1] <: L | Sequence[L] and Seq[F1] <: R | Sequence[R].

  • Since Seq[F1] <: Foo, we could bind L=Seq[F1].
  • Since Seq[F1] <: Sequence[F1], we could also bind L=F1.

So, depending on how the binding is done, one could expect one of several results:

  • list[F1], list[F1 | Seq[F1]], list[Seq[F1]]

Should a type checker pick one of these, and if so, which one and how/why? Or should all possible combinations be considered?

Playgrounds:

  1. actually, we want T | (Sequence[T] & ¬T) as in the str vs Sequence[str] issue, but type-checkers ideally should still come to the same conclusion regardless. ↩︎

2

This is a well known issue and currently intentional up to individual type checkers. Expect this to be solvable once type negation and type intersection are added, which will still take a while, but are in the works.

3

Constraint solving behaviors are unspecified in the typing spec currently. I would like to see the spec expanded to include some guidance in this area, but I don’t think it’s feasible to specify all aspects of constraint solving. It’s a complex topic that involves numerous heuristics. There are many different approaches that a type checker can use that make tradeoffs between correctness, performance, and usability.

My understanding is that ty currently has a minimal constraint solver implementation that handles only the simplest of cases. I would expect its behavior to change once the ty team implements a full-featured constraint solver.

I think we can probably all agree that if some solution exists that satisfies all of the constraints of all type variables but a type checker fails to find that solution, it should be considered a bug. For example, your table above shows that mypy generates errors for several cases where a solution exists. Such bugs can be difficult to fix without breaking other constraint solving behaviors or severely affecting analysis performance, so I’m sympathetic to the fact that mypy doesn’t find a solution here.

If a solution exists for a set of type variables, it’s often the case that multiple solutions can be found. Here’s a simple example.

def func[T](x: T, y: T) -> T: ...

reveal_type(func(0, ""))

All of the following solutions would be compatible with the constraints:

  • T = Literal[0, “”]
  • T = int | LiteralString
  • T = int | str
  • T = object

The first two potential solutions in this list have usability problems, so in practice type checkers don’t choose those. Pyright chooses the third solution, and mypy chooses the fourth. In my experience, the third solution is the best from a usability standpoint. Incidentally, pyrefly does not find any of these solutions and produces an error for this example.

The case you’re highlighting in this thread likewise results in multiple solutions. Any of them is technically correct, but some are more usable than others. Pyright employs a heuristic that is documented here.

2 Likes