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

Let's look at a slightly more involved example:

classC[T: (int,str)]:def__init__(self,t:T)->None:self.t:T=tc=C(True)

The example in the spec implies that the constructor call is fine becauseTrue is of typebool, which is a subtype ofint, andT can be instantiated toint. Thus,c should have typeC[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 writtenC[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 whenC[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 variableT with another type variableS is only allowed ifS also has constraints and each of them is also listed inT'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 wherebool gets "widened" toint. It also covers the contravariant case, where the function

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

   can be called with an argument of typeCallback[[float], None] andT gets instantiated toint. (In some sense,float gets "narrowed" toint here.)