There are a few of these that we need to recognise, actually:

• AlwaysTruthy | bool ≡ AlwaysTruthy | Literal[False]
• AlwaysFalsy | bool ≡ AlwaysFalsy | Literal[True]
• AlwaysTruthy | tuple ≡ AlwaysTruthy | tuple[()]
• AlwaysTruthy | LiteralString ≡ AlwaysTruthy | Literal[""]

Some failing tests, if anybody is interested in working on this:

--- a/crates/red_knot_python_semantic/resources/mdtest/union_types.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/union_types.md
@@ -141,3 +141,17 @@ def _(
     reveal_type(i1)  # revealed: P & Q
     reveal_type(i2)  # revealed: P & Q
 ```
+
+## Equivalent unions
+
+```py
+from typing_extensions import Literal
+from knot_extensions import is_equivalent_to, AlwaysTruthy, AlwaysFalsy, static_assert, Intersection
+
+static_assert(is_equivalent_to(AlwaysTruthy | bool, AlwaysTruthy | Literal[False]))
+static_assert(is_equivalent_to(AlwaysFalsy | bool, AlwaysFalsy | Literal[True]))
+static_assert(is_equivalent_to(AlwaysTruthy | tuple, AlwaysTruthy | tuple[()]))
+static_assert(is_equivalent_to(AlwaysTruthy | LiteralString, AlwaysTruthy | Literal[""]))
+```

This (and the complexity of our existing handling of bool in unions and intersections) makes me wonder if it would be simpler if we always eagerly decomposed bool to Literal[False] | Literal[True] in a union, and then just collected it back to bool at display time? We already collect literal types in union display, so collecting these two together and displaying them as bool shouldn't be hard.

This would be generally in line with "one internal representation for equivalent things."

This means that intersections with bool (e.g. bool & P) would technically become (Literal[True] & P) | (Literal[False] & P). But I think this would actually be OK, because Literal[True] and Literal[False] are both singleton types, which should mean any intersection with either of them always simplifies to either Never or to Literal[True/False] itself, meaning bool & P would never actually remain a union-of-intersections, it must always simplify down to either Never, either Literal[True] or Literal[False], or Literal[True] | Literal[False].

Yes, that sounds reasonable to me! I agree that this one seems like a bit of a pain to work into our existing infrastructure without doing something like that

This (and the complexity of our existing handling of bool in unions and intersections) makes me wonder if it would be simpler if we always eagerly decomposed bool to Literal[False] | Literal[True] in a union, and then just collected it back to bool at display time? We already collect literal types in union display, so collecting these two together and displaying them as bool shouldn't be hard.

This works for the bool case, but the LiteralString case is harder to fix because of the fact that we don't have a dedicated type for "all the literal strings except for Literal[""]". As well as the invariant I mentioned above (AlwaysTruthy | LiteralString ≡ AlwaysTruthy | Literal[""]), the property tests inform me that we also have at least two others that we must respect when simplifying and comparing unions:

• AlwaysTruthy | LiteralString ≡ AlwaysTruthy | Literal[""]
• ~AlwaysFalsy | LiteralString ≡ ~AlwaysFalsy | Literal[""]
• AlwaysTruthy | AlwaysFalsy | LiteralString ≡ AlwaysTruthy | AlwaysFalsy

Ah... and even with the bool case, decomposing bool to Literal[True] | Literal[False] only in the context of unions causes its own problems. Now bool is no longer a subtype of bool | str, because bool remains bool but bool | str becomes Literal[True] | Literal[False] | str. This causes the stable property test all_fully_static_type_pairs_are_subtype_of_their_union to start failing. Should we decompose bool to Literal[True, False] everywhere?

Now bool is no longer a subtype of bool | str

Would this be solved by a special case in is_equivalent_to encoding the equivalence of bool to Literal[True] | Literal[False]?

I guess if our aim is to prefer "one representation for one type" then we should prefer to decompose everywhere or nowhere. But I don't think decomposing everywhere is really an option, as we need the typeshed stub for the bool type to tell us a lot of things about the bool type.