As I mentioned above, the job of a constraint solver is to determine all of the constraints on a type variable for a given function call. Based on these constraints, it then attempts to find some type (preferably, an “optimal” type by some definition of the word “optimal”) that satisfies all of the constraints.

These constraints come from various sources:

- Upper bounds on the type variable, in the case of normal TypeVars
- Value constraints, in the case of value-constrained TypeVars
- Variance rules
- (Bidirectional) inference context
- Explicit specialization, in the case of constructor calls
- Arguments passed to the call

Let’s examine a few of your examples in detail. This might help clarify the behaviors in your mind.

**Example 1: **`constrained(x, y)`

Here we are using a value-constrained TypeVar, and the solution must match one of the specified value constraints exactly. That means we start with the constraint that the solution to `_T`

must be either `str`

or `int`

.

The first argument `x`

imposes the constraint `_T = str`

. The second argument imposes the constraint `_T = int`

. There is no possible type that satisfies these constraints, so this is an error.

**Example 2: **`arg(1, str_to_int)`

In this case, there is no upper bound, value constraint, inference context, or explicit specialization. All of the constraints come from arguments and variance rules.

The first argument `1`

is of type `int`

, and it imposes the constraint `_T ≥ int`

. This is a covariant context.

The second argument `str_to_int`

is of type `(x: str) -> int`

, and it imposes the constraint `_T ≤ str`

. This is a contravariant context because it’s an input parameter for a Callable. That explains why the constraint uses `≤`

rather than `≥`

.

There is no type that can possibly satisfy both of these constraints, hence the error.

**Example 3: **`ret(1, str)`

Once again, all of the constraints come from arguments and variance rules.

The first argument `1`

once again imposes the constraint `_T ≥ int`

. This is a covariant context.

The second argument `str`

is of type `type[str]`

and can be converted to a callable type because it’s a class object with a constructor. The converted type is effectively `(object) -> str`

. This imposes the constraint `_T ≥ str`

. This is a covariant context because it’s a return type for a Callable.

These two constraints allow for solutions `str | int`

or `object`

.

Note: I’ve left out a bunch of details above such as handling of literal types and handling of overloaded constructors when converting to a callable, but I wanted to keep the examples relatively simple.