Use generics solver to induct into the bounds of Self

Author: sharkdp

crates/ty_python_semantic/resources/mdtest/generics/legacy/functions.md

@@ -366,31 +366,6 @@ reveal_type(f(g("a")))  # revealed: tuple[Literal["a"] | None, int]
 reveal_type(g(f("a")))  # revealed: tuple[Literal["a"], int] | None
 ```
 
-## Passing generic functions to generics functions
-
-```py
-from typing import Callable, TypeVar
-
-A = TypeVar("A")
-B = TypeVar("B")
-T = TypeVar("T")
-
-def invoke(fn: Callable[[A], B], value: A) -> B:
-    return fn(value)
-
-def identity(x: T) -> T:
-    return x
-
-def head(xs: list[T]) -> T:
-    return xs[0]
-
-# TODO: this should be `Literal[1]`
-reveal_type(invoke(identity, 1))  # revealed: Unknown
-
-# TODO: this should be `Unknown | int`
-reveal_type(invoke(head, [1, 2, 3]))  # revealed: Unknown
-```
-
 ## Opaque decorators don't affect typevar binding
 
 Inside the body of a generic function, we should be able to see that the typevars bound by that

crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md

@@ -323,27 +323,6 @@ reveal_type(f(g("a")))  # revealed: tuple[Literal["a"] | None, int]
 reveal_type(g(f("a")))  # revealed: tuple[Literal["a"], int] | None
 ```
 
-## Passing generic functions to generics functions
-
-```py
-from typing import Callable
-
-def invoke[A, B](fn: Callable[[A], B], value: A) -> B:
-    return fn(value)
-
-def identity[T](x: T) -> T:
-    return x
-
-def head[T](xs: list[T]) -> T:
-    return xs[0]
-
-# TODO: this should be `Literal[1]`
-reveal_type(invoke(identity, 1))  # revealed: Unknown
-
-# TODO: this should be `Unknown | int`
-reveal_type(invoke(head, [1, 2, 3]))  # revealed: Unknown
-```
-
 ## Protocols as TypeVar bounds
 
 Protocol types can be used as TypeVar bounds, just like nominal types.

crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md

@@ -342,7 +342,6 @@ class Contravariant[T]:
 def _(x: object):
     if isinstance(x, Contravariant):
         reveal_type(x)  # revealed: Contravariant[Never]
-        # error: [invalid-argument-type] "Argument to bound method `push` is incorrect: Argument type `Contravariant[Never]` does not satisfy upper bound `Contravariant[T@Contravariant]` of type variable `Self`"
         # error: [invalid-argument-type] "Argument to bound method `push` is incorrect: Expected `Never`, found `Literal[42]`"
         x.push(42)
 ```

crates/ty_python_semantic/src/types.rs

@@ -1631,31 +1631,6 @@ impl<'db> Type<'db> {
             // be specialized to `Never`.)
             (_, Type::NonInferableTypeVar(_)) => ConstraintSet::from(false),
 
-            (Type::TypeVar(_), _) if relation.is_assignability() => {
-                // The implicit lower bound of a typevar is `Never`, which means
-                // that it is always assignable to any other type.
-
-                // TODO: record the unification constraints
-
-                ConstraintSet::from(true)
-            }
-
-            (_, Type::TypeVar(typevar))
-                if relation.is_assignability()
-                    && typevar.typevar(db).upper_bound(db).is_none_or(|bound| {
-                        !self
-                            .has_relation_to_impl(db, bound, relation, visitor)
-                            .is_never_satisfied()
-                    }) =>
-            {
-                // TODO: record the unification constraints
-
-                typevar
-                    .typevar(db)
-                    .upper_bound(db)
-                    .when_none_or(|bound| self.has_relation_to_impl(db, bound, relation, visitor))
-            }
-
             // TODO: Infer specializations here
             (Type::TypeVar(_), _) | (_, Type::TypeVar(_)) => ConstraintSet::from(false),
 

crates/ty_python_semantic/src/types/generics.rs

@@ -499,9 +499,9 @@ fn is_subtype_in_invariant_position<'db>(
         // leads to union simplification, which means that we lose track
         // of type variables without recording the constraints under which
         // the relation holds.
-        if matches!(base, Type::TypeVar(_)) || matches!(derived, Type::TypeVar(_)) {
-            return ConstraintSet::from(true);
-        }
+        // if matches!(base, Type::TypeVar(_)) || matches!(derived, Type::TypeVar(_)) {
+        //     return ConstraintSet::from(true);
+        // }
 
         derived.has_relation_to_impl(db, base, TypeRelation::Subtyping, visitor)
     };
@@ -1039,6 +1039,11 @@ impl<'db> SpecializationBuilder<'db> {
     }
 
     fn add_type_mapping(&mut self, bound_typevar: BoundTypeVarInstance<'db>, ty: Type<'db>) {
+        dbg!(
+            bound_typevar.typevar(self.db).name(self.db),
+            &ty.display(self.db)
+        );
+
         self.types
             .entry(bound_typevar)
             .and_modify(|existing| {
@@ -1116,7 +1121,14 @@ impl<'db> SpecializationBuilder<'db> {
             (Type::TypeVar(bound_typevar), ty) | (ty, Type::TypeVar(bound_typevar)) => {
                 match bound_typevar.typevar(self.db).bound_or_constraints(self.db) {
                     Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
-                        if !ty.is_assignable_to(self.db, bound) {
+                        let skip_assignability_check =
+                            if bound_typevar.typevar(self.db).is_self(self.db) {
+                                self.infer(ty, bound).is_ok()
+                            } else {
+                                false
+                            };
+
+                        if !(skip_assignability_check || ty.is_assignable_to(self.db, bound)) {
                             return Err(SpecializationError::MismatchedBound {
                                 bound_typevar,
                                 argument: ty,
@@ -1137,7 +1149,9 @@ impl<'db> SpecializationBuilder<'db> {
                         });
                     }
                     _ => {
-                        self.add_type_mapping(bound_typevar, ty);
+                        if !matches!(ty, Type::TypeVar(_)) {
+                            self.add_type_mapping(bound_typevar, ty);
+                        }
                     }
                 }
             }