Support for alternative generic inference algorithms

I believe there is a use case for generic inference that doesn't get as wide as possible.

Look at this example of an assertion function, you would never want to do an assertion between two different types, but there is currently no way to type this:

from typing import TypeVar

T = TypeVar("T")

def assert_something(expected: T, actual: T) -> None:
    ...

assert_something(1, "")  # no error, SUS alert!, T is inferred as `object`

Here are some behaviors from other languages

TypeScript

In Typescript generic inference is narrowed to type level types(not down to instance level types) and is never widened:

function assertSomething<T>(expected: T, actual: T): void { ... }

assertSomething(1, "")  // Argument of type 'string' is not assignable to parameter of type 'number'.

Kotlin

Kotlin by default acts the same as Python, but there are annotations for changing the behavior of inference.

NoInfer will exclude that usage from inferring the type.

fun <T> assertSomething(expected: T, actual: @NoInfer T) { }
assertSomething(1, "")  // Type mismatch: inferred type is String but Int was expected

Exact will require the type of the parameter is equal at a type level (Number != Int)

fun <T> foo(x: @Exact T) { }
foo<Number>(1) // Type mismatch. Required: Number, Found: Int

OnlyInputTypes will require a type annotation if there is any difference in types between the usages of the generic:

fun <@OnlyInputTypes T> doSomething(a: T, b: T)  { }

val a = doSomething("a", "b")
val b = doSomething("a", 1) // Type inference failed. The value of the type parameter T should be mentioned in input types (argument types, receiver type or expected type). Try to specify it explicitly.

Comienza comparando el ejemplo de Python con los comportamientos de inferencia de TypeScript y Kotlin descritos en el issue. Define qué algoritmos alternativos de inferencia o anotaciones deben admitirse y cómo se espera que se comporten los tipos de argumentos mixtos, los tipos exactos y la inferencia excluida; completar esto requeriría un diseño acordado y la especificación de tipado correspondiente.