[red-knot] more precise types from chained boolean expressions

[carljm]

As pointed out by @Slyces in #13571 (comment)

Copying my comments from there:

I think the logic here is that when we have an actual bool type in a chained boolean expression, in non-last-position, rather than adding bool to the union we can instead add Literal[False] (for AND) or Literal[True] (for OR).

There's a more generalized version of this where we add Falsy and Truthy types, and then we'd always intersect any type in that position (not just bool) with Falsy or Truthy, and then for bools that would simplify out in the intersection (e.g. bool & Falsy is Literal[False]). I think it's likely we end up doing this for type narrowing anyway, but I don't have strong feelings about whether we go straight for the generalized solution or start with a bool-specific implementation.

[Slyces]

If I understand correctly

• We have 2 new variants Type::Truthy and Type::Falsy
• They only make sense in intersections (?)
  • A & Truthy -> subset of instances of A that evaluate to True
  • A & Falsy -> subset of instances of A that evaluate to False (0 for int/float, "" for str, ...)

I have some questions:

• Would those new variants make sense outside of intersections?
• Would we display those variants? I think I see the use - we understand that it's not "any" A - but would this ever make it to the end user?
  • If we answer no (it's purely internal to have more precise information) how do we ensure this doesn't leak?

[carljm]

Those are great questions!

Any type "makes sense" independently as long as we can describe it as some set of possible runtime values. So these types can stand alone, in principle: Type::Falsy is the set of all objects whose __bool__ method (always) returns False, and vice versa for Type::Truthy.

In practice, I expect that we would only create these types in intersections, wherever we are able to determine that a type must be truthy or falsy.

If we introduce this type, we accept (at least for now) the fact that it may leak to users, since we won't be able to simplify it in all cases. We will often have this tradeoff, where we can more fully represent our type knowledge, at the cost of displaying more complex types to users. In general, I would prefer to represent the most precise type knowledge we can be confident of, and then find ways to simplify the user type display if that proves to be necessary. For instance, we could later implement logic in the display code for intersections to just hide these types in the output, if we end up feeling that it becomes too noisy otherwise. My hope, though, is that users will find these types reasonably intuitive, and will appreciate more precise typing.

One thing to note here is that currently (since we've so far only implemented support for one form of narrowing, is not None), intersections don't occur often; implementing this issue will add another case where intersections appear, and may require adding support for intersections in more places in order to get useful test results.