What type annotation should I use to type a function that accept a type T and a value of that type using typing in Python?

I never really used Generics in the past and this is my first time using mypy in Python, but I'm trying to type a function that both accept a class and a value of that class using the typing module

So far I made this, but in both uses, mypy does not raise any error when I use the command mypy file.py. Am I doing something wrong ?

# file.py
from typing import TypeVar, Type, Any


T = TypeVar("T")

def function(cls: Type[T], inst: T) -> bool: 
    # Should be true for all values matching the type annotation
    return isinstance(inst, cls) 


function(int, 5) # Correct
function(str, 5) # Incorrect - mypy should be raising an error here

Solution

When determining which type T is actually bound to, mypy looks at both arguments and choose a type that will satisfy each, rather than trying to use one to restrict options available for the other. When you call

function(str, 5)

mypy choose to bind object to T: this works because 5 is an instance of object and str is a subclass of object.

I don't think there is a general solution to this. For more specific cases, you can enumerate a list of types that can be bound to T, which can prevent a too-general superclass from being chosen. For example, given

T = TypeVar('T', str, int)

only str or int, not object, can be bound to T when typechecking function. This means the following are OK:

function(str, "5")  # T ~ str
function(int, 5)  # T ~ int

but this is not:

function(str, 5)  # Neither T ~ str nor T ~ int satisfy the type hints.

To force you to think about what restrictions you really want to put on T to disallow function(str, 5), consider the following:

function(int, True)

Do you want that to fail? If so, you are violating a fundamental tenet of type checking, which says you can use a value of type a anywhere a value of type b is expected, as long as a is a subtype of b.

Do you want that to succeed? Then you need to figure out why binding T ~ int is acceptable but binding T ~ object is not. I'm not sure you can do that, again, without violating the fundamental tenet stated above.