[red-knot] Proper handling of empty intersections and Never.

[sharkdp]

I found this while creating the type Literal[1, 2, 3] & ~Literal[1] & ~Literal[2]. I was expecting to get Literal[3] after all simplifications were applied, but I got ~Literal[2] | Literal[3] instead. This is clearly not optimal.

The reason for this behavior is the following (using 1 instead of Literal[1] etc): When adding the first negation, we get the following in the union-of-intersections representation:

  (1 | 2 | 3) & ~1
= (1 & ~1 | 2 & ~1 | 3 & ~1)

In the second and third component, the simplification creates 2 & ~1 = 2 and 3 & ~1 = 3, as expected. In the first component, the current implementation of simplification removes all positive (1) and negative (~1) components from the intersection, leaving an empty intersection:

= (empty-intersection | 2 | 3)

The idea was that the empty-intersection would represent Never (similar to how IntersectionBuilder::build() returns Never for the empty-empty case). But an empty intersection should actually represent the type object. To represent Never, we would need to explicitly add Never to the positive side. Since we don't do that, we end up creating

  (empty-intersection | 2 | 3) & ~2
= (~2 | 2 & ~2 | 3 & ~2)
= ~2 | Never | 3
= ~2 | 3

in the second step.

[sharkdp]

Hey GitHub, I said "while trying to fix #13876" in that PR.

[sharkdp]

The fundamental problem is the following. In bindings_ty, we use IntersectionBuilder::add_positive with constraints, as if that would mean: build the intersection with the existing binding_ty type:

ruff/crates/red_knot_python_semantic/src/types.rs

Lines 156 to 161 in 7dbd8f0

	builder = builder
	.add_positive(binding_ty)
	.add_positive(first_constraint_ty);
	for constraint_ty in constraint_tys {
	builder = builder.add_positive(constraint_ty);
	}

But the intersection between A & B is subtly different from IB::new().add_positive(A).add_positive(B).build(), if A and/or B are intersections themselves. For example, if A = {pos = [p]; neg = []} and B = {pos = []; neg = [n]}, using .add_positive(A).add_positive(B) will result in an intersection with {pos = [p]; neg = [n]}. However, B is actually Never, so the intersection between A & B is also Never.

Note: Those intermediate empty positive/negative lists can appear while building up a larger intersection type (due to simplification), which is exactly what happens in the code above.

I will try to fix this by adding a Type::intersect method.