[ty] Consider domain of BDD when checking whether always satisfiable (#21050)

That PR title might be a bit inscrutable.

Consider the two constraints `T ≤ bool` and `T ≤ int`. Since `bool ≤
int`, by transitivity `T ≤ bool` implies `T ≤ int`. (Every type that is
a subtype of `bool` is necessarily also a subtype of `int`.) That means
that `T ≤ bool ∧ T ≰ int` is an impossible combination of constraints,
and is therefore not a valid input to any BDD. We say that that
assignment is not in the _domain_ of the BDD.

The implication `T ≤ bool → T ≤ int` can be rewritten as `T ≰ bool ∨ T ≤
int`. (That's the definition of implication.) If we construct that
constraint set in an mdtest, we should get a constraint set that is
always satisfiable. Previously, that constraint set would correctly
_display_ as `always`, but a `static_assert` on it would fail.

The underlying cause is that our `is_always_satisfied` method would only
test if the BDD was the `AlwaysTrue` terminal node. `T ≰ bool ∨ T ≤ int`
does not simplify that far, because we purposefully keep around those
constraints in the BDD structure so that it's easier to compare against
other BDDs that reference those constraints.

To fix this, we need a more nuanced definition of "always satisfied".
Instead of evaluating to `true` for _every_ input, we only need it to
evaluate to `true` for every _valid_ input — that is, every input in its
domain.

crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md

@@ -604,6 +604,8 @@ def _[T, U]() -> None:
 
 ## Other simplifications
 
+### Displaying constraint sets
+
 When displaying a constraint set, we transform the internal BDD representation into a DNF formula
 (i.e., the logical OR of several clauses, each of which is the logical AND of several constraints).
 This section contains several examples that show that we simplify the DNF formula as much as we can
@@ -626,11 +628,44 @@ def f[T, U]():
     reveal_type((t1 | t2) & (u1 | u2))
 ```
 
+We might simplify a BDD so much that we can no longer see the constraints that we used to construct
+it!
+
+```py
+from typing import Never
+from ty_extensions import static_assert
+
+def f[T]():
+    t_int = range_constraint(Never, T, int)
+    t_bool = range_constraint(Never, T, bool)
+
+    # `T ≤ bool` implies `T ≤ int`: if a type satisfies the former, it must always satisfy the
+    # latter. We can turn that into a constraint set, using the equivalence `p → q == ¬p ∨ q`:
+    implication = ~t_bool | t_int
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(implication)
+    static_assert(implication)
+
+    # However, because of that implication, some inputs aren't valid: it's not possible for
+    # `T ≤ bool` to be true and `T ≤ int` to be false. This is reflected in the constraint set's
+    # "domain", which maps valid inputs to `true` and invalid inputs to `false`. This means that two
+    # constraint sets that are both always satisfied will not be identical if they have different
+    # domains!
+    always = range_constraint(Never, T, object)
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(always)
+    static_assert(always)
+    static_assert(implication != always)
+```
+
+### Normalized bounds
+
 The lower and upper bounds of a constraint are normalized, so that we equate unions and
 intersections whose elements appear in different orders.
 
 ```py
 from typing import Never
+from ty_extensions import range_constraint
 
 def f[T]():
     # revealed: ty_extensions.ConstraintSet[(T@f ≤ int | str)]