Spec for subtypes of type variable constraints too vague

The spec is very vague when it comes to instantiating a type variable with constraints with a subtype of one of the constraints:

https://github.com/python/typing/blob/b806c04133760efee732ce5081b177d84def22fe/docs/spec/generics.rst?plain=1#L71-L81

Let's look at a slightly more involved example:

class C[T: (int, str)]:
    def __init__(self, t: T) -> None:
        self.t: T = t

c = C(True)

The example in the spec implies that the constructor call is fine because True is of type bool, which is a subtype of int, and T can be instantiated to int. Thus, c should have type C[int]. This makes perfect sense and is totally natural if you write a bidirectional type checker anyway. Nothing controversial here.

What about the following?

c: C[bool] = ...

Does the type "widening" to the base type mentioned in the spec apply here too and this has to be interpreted as if the user had written C[int]? At least pyright interprets it this way. I'm wondering if this was the intent of the spec? Off the top of my head, I cannot think of a situation where this would be a useful feature (but I'm happy to convinced otherwise). Moreover, this can become rather counter-intuitive when C[bool] appears in contravariant positions.

I would like to get a conversation going that crystallizes the intent of the spec in this regard. If we come to a conclusion, I'd be more than happy to update the docs to reflect this outcome.

Here's how I would roughly specify the feature:

1. Explicit instantiations of constrained type variables via class/alias specializations must be taken at face value and not automatically be widened to base types. If the explicitly mentioned type argument is neither a type variable nor a type equivalent to one of the constraints, that's a type error. For the exact meaning of "equivalent", I would suggest to pick an equivalence relation on the more syntactic side of the spectrum of possibilities but haven't thought about this aspect too deeply so far.

2. Explicitly instantiating a constrained type variable T with another type variable S is only allowed if S also has constraints and each of them is also listed in T's constraints (up to the same equivalence as above). (I avoided the word "subset" on purpose since that's too easy to interpret as "subtype", which I do not mean!)

3. All of this this should also apply to generic functions should there ever be a way to explicitly specialize them.

4. When inferring type arguments for generic function calls, including constructor calls, the function is conceptually "exploded" into an overloaded function with one case for each constraint and overload resolution decides which constraint to pick as the instantiation for the type variable.

   This gets particularly gnarly in the presence of multiple matching constraints caused by multiple inheritance. Being consistent with overload resolution seems like a good property to have here.

   This covers the covariant case illustrated in the example above where bool gets "widened" to int. It also covers the contravariant case, where the function

   def higher_order[T: (int, str)](f: Callback[[T], None]): ...
   

   can be called with an argument of type Callback[[float], None] and T gets instantiated to int. (In some sense, float gets "narrowed" to int here.)

Start with docs/spec/generics.rst, especially the linked section on constrained type variables, and review the examples involving C[bool], constructor inference, and contravariant positions. Read the four proposed rules and the existing comment discussion before determining the intended semantics. Done means reaching agreement and updating the specification to state the behavior clearly.