[red-knot] Gradual forms do not participate in equivalence/subtyping (#14758)

## Summary

This changeset contains various improvements concerning non-fully-static
types and their relationships:

- Make sure that non-fully-static types do not participate in
equivalence or subtyping.
- Clarify what `Type::is_equivalent_to` actually implements.
- Introduce `Type::is_fully_static`
- New tests making sure that multiple `Any`/`Unknown`s inside unions and
intersections are collapsed.

closes #14524

## Test Plan

- Added new unit tests for union and intersection builder
- Added new unit tests for `Type::is_equivalent_to`
- Added new unit tests for `Type::is_subtype_of`
- Added new property test making sure that non-fully-static types do not
participate in subtyping

Author: sharkdp

crates/red_knot_python_semantic/src/types.rs

@@ -302,13 +302,7 @@ fn declarations_ty<'db>(
     let declared_ty = if let Some(second) = all_types.next() {
         let mut builder = UnionBuilder::new(db).add(first);
         for other in [second].into_iter().chain(all_types) {
-            // Make sure not to emit spurious errors relating to `Type::Todo`,
-            // since we only infer this type due to a limitation in our current model.
-            //
-            // `Unknown` is different here, since we might infer `Unknown`
-            // for one of these due to a variable being defined in one possible
-            // control-flow branch but not another one.
-            if !first.is_equivalent_to(db, other) && !first.is_todo() && !other.is_todo() {
+            if !first.is_equivalent_to(db, other) {
                 conflicting.push(other);
             }
             builder = builder.add(other);
@@ -600,11 +594,16 @@ impl<'db> Type<'db> {
 
     /// Return true if this type is a [subtype of] type `target`.
     ///
+    /// This method returns `false` if either `self` or `other` is not fully static.
+    ///
     /// [subtype of]: https://typing.readthedocs.io/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence
     pub(crate) fn is_subtype_of(self, db: &'db dyn Db, target: Type<'db>) -> bool {
         if self.is_equivalent_to(db, target) {
             return true;
         }
+        if !self.is_fully_static(db) || !target.is_fully_static(db) {
+            return false;
+        }
         match (self, target) {
             (Type::Unknown | Type::Any | Type::Todo(_), _) => false,
             (_, Type::Unknown | Type::Any | Type::Todo(_)) => false,
@@ -764,8 +763,16 @@ impl<'db> Type<'db> {
         }
     }
 
-    /// Return true if this type is equivalent to type `other`.
+    /// Return true if this type is [equivalent to] type `other`.
+    ///
+    /// This method returns `false` if either `self` or `other` is not fully static.
+    ///
+    /// [equivalent to]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-equivalent
     pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Type<'db>) -> bool {
+        if !(self.is_fully_static(db) && other.is_fully_static(db)) {
+            return false;
+        }
+
         // TODO equivalent but not identical structural types, differently-ordered unions and
         // intersections, other cases?
 
@@ -776,7 +783,6 @@ impl<'db> Type<'db> {
         // of `NoneType` and `NoDefaultType` in typeshed. This should not be required anymore once
         // we understand `sys.version_info` branches.
         self == other
-            || matches!((self, other), (Type::Todo(_), Type::Todo(_)))
             || matches!((self, other),
                 (
                     Type::Instance(InstanceType { class: self_class }),
@@ -790,6 +796,17 @@ impl<'db> Type<'db> {
             )
     }
 
+    /// Returns true if both `self` and `other` are the same gradual form
+    /// (limited to `Any`, `Unknown`, or `Todo`).
+    pub(crate) fn is_same_gradual_form(self, other: Type<'db>) -> bool {
+        matches!(
+            (self, other),
+            (Type::Unknown, Type::Unknown)
+                | (Type::Any, Type::Any)
+                | (Type::Todo(_), Type::Todo(_))
+        )
+    }
+
     /// Return true if this type and `other` have no common elements.
     ///
     /// Note: This function aims to have no false positives, but might return
@@ -996,6 +1013,63 @@ impl<'db> Type<'db> {
         }
     }
 
+    /// Returns true if the type does not contain any gradual forms (as a sub-part).
+    pub(crate) fn is_fully_static(self, db: &'db dyn Db) -> bool {
+        match self {
+            Type::Any | Type::Unknown | Type::Todo(_) => false,
+            Type::Never
+            | Type::FunctionLiteral(..)
+            | Type::ModuleLiteral(..)
+            | Type::IntLiteral(_)
+            | Type::BooleanLiteral(_)
+            | Type::StringLiteral(_)
+            | Type::LiteralString
+            | Type::BytesLiteral(_)
+            | Type::SliceLiteral(_)
+            | Type::KnownInstance(_) => true,
+            Type::ClassLiteral(_) | Type::SubclassOf(_) | Type::Instance(_) => {
+                // TODO: Ideally, we would iterate over the MRO of the class, check if all
+                // bases are fully static, and only return `true` if that is the case.
+                //
+                // This does not work yet, because we currently infer `Unknown` for some
+                // generic base classes that we don't understand yet. For example, `str`
+                // is defined as `class str(Sequence[str])` in typeshed and we currently
+                // compute its MRO as `(str, Unknown, object)`. This would make us think
+                // that `str` is a gradual type, which causes all sorts of downstream
+                // issues because it does not participate in equivalence/subtyping etc.
+                //
+                // Another problem is that we run into problems if we eagerly query the
+                // MRO of class literals here. I have not fully investigated this, but
+                // iterating over the MRO alone, without even acting on it, causes us to
+                // infer `Unknown` for many classes.
+
+                true
+            }
+            Type::Union(union) => union
+                .elements(db)
+                .iter()
+                .all(|elem| elem.is_fully_static(db)),
+            Type::Intersection(intersection) => {
+                intersection
+                    .positive(db)
+                    .iter()
+                    .all(|elem| elem.is_fully_static(db))
+                    && intersection
+                        .negative(db)
+                        .iter()
+                        .all(|elem| elem.is_fully_static(db))
+            }
+            Type::Tuple(tuple) => tuple
+                .elements(db)
+                .iter()
+                .all(|elem| elem.is_fully_static(db)),
+            // TODO: Once we support them, make sure that we return `false` for other types
+            // containing gradual forms such as `tuple[Any, ...]` or `Callable[..., str]`.
+            // Conversely, make sure to return `true` for homogeneous tuples such as
+            // `tuple[int, ...]`, once we add support for them.
+        }
+    }
+
     /// Return true if there is just a single inhabitant for this type.
     ///
     /// Note: This function aims to have no false positives, but might return `false`
@@ -3261,7 +3335,9 @@ pub(crate) mod tests {
     }
 
     #[test_case(Ty::BuiltinInstance("object"), Ty::BuiltinInstance("int"))]
+    #[test_case(Ty::Unknown, Ty::Unknown)]
     #[test_case(Ty::Unknown, Ty::IntLiteral(1))]
+    #[test_case(Ty::Any, Ty::Any)]
     #[test_case(Ty::Any, Ty::IntLiteral(1))]
     #[test_case(Ty::IntLiteral(1), Ty::Unknown)]
     #[test_case(Ty::IntLiteral(1), Ty::Any)]
@@ -3369,6 +3445,18 @@ pub(crate) mod tests {
         assert!(from.into_type(&db).is_equivalent_to(&db, to.into_type(&db)));
     }
 
+    #[test_case(Ty::Any, Ty::Any)]
+    #[test_case(Ty::Any, Ty::None)]
+    #[test_case(Ty::Unknown, Ty::Unknown)]
+    #[test_case(Ty::Todo, Ty::Todo)]
+    #[test_case(Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(0)]))]
+    #[test_case(Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2), Ty::IntLiteral(3)]))]
+    fn is_not_equivalent_to(from: Ty, to: Ty) {
+        let db = setup_db();
+
+        assert!(!from.into_type(&db).is_equivalent_to(&db, to.into_type(&db)));
+    }
+
     #[test_case(Ty::Never, Ty::Never)]
     #[test_case(Ty::Never, Ty::None)]
     #[test_case(Ty::Never, Ty::BuiltinInstance("int"))]
@@ -3597,6 +3685,41 @@ pub(crate) mod tests {
         assert!(!from.into_type(&db).is_singleton(&db));
     }
 
+    #[test_case(Ty::Never)]
+    #[test_case(Ty::None)]
+    #[test_case(Ty::IntLiteral(1))]
+    #[test_case(Ty::BooleanLiteral(true))]
+    #[test_case(Ty::StringLiteral("abc"))]
+    #[test_case(Ty::LiteralString)]
+    #[test_case(Ty::BytesLiteral("abc"))]
+    #[test_case(Ty::KnownClassInstance(KnownClass::Str))]
+    #[test_case(Ty::KnownClassInstance(KnownClass::Object))]
+    #[test_case(Ty::KnownClassInstance(KnownClass::Type))]
+    #[test_case(Ty::BuiltinClassLiteral("str"))]
+    #[test_case(Ty::TypingLiteral)]
+    #[test_case(Ty::Union(vec![Ty::KnownClassInstance(KnownClass::Str), Ty::None]))]
+    #[test_case(Ty::Intersection{pos: vec![Ty::KnownClassInstance(KnownClass::Str)], neg: vec![Ty::LiteralString]})]
+    #[test_case(Ty::Tuple(vec![]))]
+    #[test_case(Ty::Tuple(vec![Ty::KnownClassInstance(KnownClass::Int), Ty::KnownClassInstance(KnownClass::Object)]))]
+    fn is_fully_static(from: Ty) {
+        let db = setup_db();
+
+        assert!(from.into_type(&db).is_fully_static(&db));
+    }
+
+    #[test_case(Ty::Any)]
+    #[test_case(Ty::Unknown)]
+    #[test_case(Ty::Todo)]
+    #[test_case(Ty::Union(vec![Ty::Any, Ty::KnownClassInstance(KnownClass::Str)]))]
+    #[test_case(Ty::Union(vec![Ty::KnownClassInstance(KnownClass::Str), Ty::Unknown]))]
+    #[test_case(Ty::Intersection{pos: vec![Ty::Any], neg: vec![Ty::LiteralString]})]
+    #[test_case(Ty::Tuple(vec![Ty::KnownClassInstance(KnownClass::Int), Ty::Any]))]
+    fn is_not_fully_static(from: Ty) {
+        let db = setup_db();
+
+        assert!(!from.into_type(&db).is_fully_static(&db));
+    }
+
     #[test_case(Ty::IntLiteral(1); "is_int_literal_truthy")]
     #[test_case(Ty::IntLiteral(-1))]
     #[test_case(Ty::StringLiteral("foo"))]
@@ -3771,19 +3894,6 @@ pub(crate) mod tests {
         let todo3 = todo_type!();
         let todo4 = todo_type!();
 
-        assert!(todo1.is_equivalent_to(&db, todo2));
-        assert!(todo3.is_equivalent_to(&db, todo4));
-        assert!(todo1.is_equivalent_to(&db, todo3));
-
-        assert!(todo1.is_subtype_of(&db, todo2));
-        assert!(todo2.is_subtype_of(&db, todo1));
-
-        assert!(todo3.is_subtype_of(&db, todo4));
-        assert!(todo4.is_subtype_of(&db, todo3));
-
-        assert!(todo1.is_subtype_of(&db, todo3));
-        assert!(todo3.is_subtype_of(&db, todo1));
-
         let int = KnownClass::Int.to_instance(&db);
 
         assert!(int.is_assignable_to(&db, todo1));

crates/red_knot_python_semantic/src/types/builder.rs

@@ -73,7 +73,8 @@ impl<'db> UnionBuilder<'db> {
                         // supertype of bool. Therefore, we are done.
                         break;
                     }
-                    if ty.is_subtype_of(self.db, *element) {
+
+                    if ty.is_same_gradual_form(*element) || ty.is_subtype_of(self.db, *element) {
                         return self;
                     } else if element.is_subtype_of(self.db, ty) {
                         to_remove.push(index);
@@ -259,7 +260,9 @@ impl<'db> InnerIntersectionBuilder<'db> {
             let mut to_remove = SmallVec::<[usize; 1]>::new();
             for (index, existing_positive) in self.positive.iter().enumerate() {
                 // S & T = S    if S <: T
-                if existing_positive.is_subtype_of(db, new_positive) {
+                if existing_positive.is_subtype_of(db, new_positive)
+                    || existing_positive.is_same_gradual_form(new_positive)
+                {
                     return;
                 }
                 // same rule, reverse order
@@ -496,6 +499,17 @@ mod tests {
         assert_eq!(u1.expect_union().elements(&db), &[t1, t0]);
     }
 
+    #[test]
+    fn build_union_simplify_multiple_unknown() {
+        let db = setup_db();
+        let t0 = KnownClass::Str.to_instance(&db);
+        let t1 = Type::Unknown;
+
+        let u = UnionType::from_elements(&db, [t0, t1, t1]);
+
+        assert_eq!(u.expect_union().elements(&db), &[t0, t1]);
+    }
+
     #[test]
     fn build_union_subsume_multiple() {
         let db = setup_db();
@@ -603,6 +617,42 @@ mod tests {
         assert_eq!(ty, Type::Never);
     }
 
+    #[test]
+    fn build_intersection_simplify_multiple_unknown() {
+        let db = setup_db();
+
+        let ty = IntersectionBuilder::new(&db)
+            .add_positive(Type::Unknown)
+            .add_positive(Type::Unknown)
+            .build();
+        assert_eq!(ty, Type::Unknown);
+
+        let ty = IntersectionBuilder::new(&db)
+            .add_positive(Type::Unknown)
+            .add_negative(Type::Unknown)
+            .build();
+        assert_eq!(ty, Type::Unknown);
+
+        let ty = IntersectionBuilder::new(&db)
+            .add_negative(Type::Unknown)
+            .add_negative(Type::Unknown)
+            .build();
+        assert_eq!(ty, Type::Unknown);
+
+        let ty = IntersectionBuilder::new(&db)
+            .add_positive(Type::Unknown)
+            .add_positive(Type::IntLiteral(0))
+            .add_negative(Type::Unknown)
+            .build();
+        assert_eq!(
+            ty,
+            IntersectionBuilder::new(&db)
+                .add_positive(Type::Unknown)
+                .add_positive(Type::IntLiteral(0))
+                .build()
+        );
+    }
+
     #[test]
     fn intersection_distributes_over_union() {
         let db = setup_db();

crates/red_knot_python_semantic/src/types/property_tests.rs

@@ -213,6 +213,12 @@ mod stable {
         singleton_implies_single_valued, db,
         forall types t. t.is_singleton(db) => t.is_single_valued(db)
     );
+
+    // If `T` contains a gradual form, it should not participate in subtyping
+    type_property_test!(
+        non_fully_static_types_do_not_participate_in_subtyping, db,
+        forall types s, t. !s.is_fully_static(db) => !s.is_subtype_of(db, t) && !t.is_subtype_of(db, s)
+    );
 }
 
 /// This module contains property tests that currently lead to many false positives.