Revert back to S+ <: T- definition of gradual subtyping

Author: carljm

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

@@ -181,7 +181,7 @@ def bounded_by_gradual[T: Any](t: T) -> None:
     static_assert(is_assignable_to(T, Sub))
     static_assert(not is_assignable_to(Sub, T))
 
-    static_assert(is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(T, Any))
     static_assert(not is_subtype_of(Any, T))
     static_assert(not is_subtype_of(T, Super))
     static_assert(not is_subtype_of(Super, T))
@@ -275,7 +275,7 @@ def constrained_by_gradual[T: (Base, Any)](t: T) -> None:
     static_assert(not is_subtype_of(T, Sub))
     static_assert(not is_subtype_of(T, Unrelated))
     static_assert(not is_subtype_of(T, Any))
-    static_assert(is_subtype_of(T, Super | Any))
+    static_assert(not is_subtype_of(T, Super | Any))
     static_assert(not is_subtype_of(T, Super | Unrelated))
     static_assert(not is_subtype_of(Super, T))
     static_assert(not is_subtype_of(Base, T))
@@ -285,7 +285,7 @@ def constrained_by_gradual[T: (Base, Any)](t: T) -> None:
     static_assert(not is_subtype_of(Base | Any, T))
     static_assert(not is_subtype_of(Super | Unrelated, T))
     static_assert(not is_subtype_of(Intersection[Base, Unrelated], T))
-    static_assert(is_subtype_of(Intersection[Base, Any], T))
+    static_assert(not is_subtype_of(Intersection[Base, Any], T))
 ```
 
 Two distinct fully static typevars are not subtypes of each other, even if they have the same

crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md

@@ -329,7 +329,7 @@ Its subtyping follows the general rule for subtyping of gradual types.
 from typing import Any
 from ty_extensions import static_assert, is_subtype_of
 
-static_assert(is_subtype_of(tuple[Any, ...], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[Any, ...], tuple[Any, ...]))
 static_assert(not is_subtype_of(tuple[Any, ...], tuple[Any]))
 static_assert(not is_subtype_of(tuple[Any, ...], tuple[Any, Any]))
 static_assert(not is_subtype_of(tuple[Any, ...], tuple[int, ...]))
@@ -340,7 +340,7 @@ static_assert(not is_subtype_of(tuple[Any, ...], tuple[int, int]))
 Same applies when `tuple[Any, ...]` is unpacked into a mixed tuple.
 
 ```py
-static_assert(is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int, *tuple[Any, ...]]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int, *tuple[Any, ...]]))
 static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[Any, ...]))
 static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[Any]))
 static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[Any, Any]))
@@ -349,7 +349,7 @@ static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int, ...]))
 static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int]))
 static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int, int]))
 
-static_assert(is_subtype_of(tuple[*tuple[Any, ...], int], tuple[*tuple[Any, ...], int]))
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[*tuple[Any, ...], int]))
 static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[Any, ...]))
 static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[Any]))
 static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[Any, Any]))
@@ -358,7 +358,7 @@ static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[int, ...]))
 static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[int]))
 static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[int, int]))
 
-static_assert(is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[int, *tuple[Any, ...], int]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[int, *tuple[Any, ...], int]))
 static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[Any, ...]))
 static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[Any]))
 static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[Any, Any]))
@@ -594,13 +594,13 @@ static_assert(is_subtype_of(TypeIs[str], int))
 from ty_extensions import is_equivalent_to, is_subtype_of, static_assert
 from typing_extensions import TypeGuard, TypeIs
 
-static_assert(is_subtype_of(TypeGuard[int], TypeGuard[int]))
-static_assert(is_subtype_of(TypeGuard[bool], TypeGuard[int]))
+# TODO: TypeGuard
+# static_assert(is_subtype_of(TypeGuard[int], TypeGuard[int]))
+# static_assert(is_subtype_of(TypeGuard[bool], TypeGuard[int]))
 static_assert(is_subtype_of(TypeIs[int], TypeIs[int]))
 static_assert(is_subtype_of(TypeIs[int], TypeIs[int]))
 
-# TODO: TypeGuard
-static_assert(not is_subtype_of(TypeGuard[int], TypeGuard[bool]))  # error: [static-assert-error]
+static_assert(not is_subtype_of(TypeGuard[int], TypeGuard[bool]))
 static_assert(not is_subtype_of(TypeIs[bool], TypeIs[int]))
 static_assert(not is_subtype_of(TypeIs[int], TypeIs[bool]))
 ```
@@ -763,49 +763,44 @@ static_assert(is_subtype_of(LiteralBase | LiteralUnrelated, object))
 
 ## Non-fully-static types
 
-A non-fully-static type `A` can be considered a subtype of another type `B` if all possible
-materializations of `A` are a subtype of some possible materialization of `B`, and all possible
-materializations of `B` are a supertype of some possible materialization of `A`.
+A non-fully-static type can be considered a subtype of another type if all possible materializations
+of the first type represent sets of values that are a subset of every possible set of values
+represented by a materialization of the second type.
 
 ```py
 from ty_extensions import Unknown, is_subtype_of, static_assert, Intersection
 from typing_extensions import Any
 
-static_assert(is_subtype_of(Any, Any))
+static_assert(not is_subtype_of(Any, Any))
 static_assert(not is_subtype_of(Any, int))
 static_assert(not is_subtype_of(int, Any))
 static_assert(is_subtype_of(Any, object))
 static_assert(not is_subtype_of(object, Any))
 
 static_assert(is_subtype_of(int, Any | int))
-static_assert(is_subtype_of(Any, Any | int))
 static_assert(is_subtype_of(Intersection[Any, int], int))
 static_assert(not is_subtype_of(tuple[int, int], tuple[int, Any]))
 ```
 
 The same for `Unknown`:
 
 ```py
-static_assert(is_subtype_of(Unknown, Unknown))
-static_assert(is_subtype_of(Any, Unknown))
-static_assert(is_subtype_of(Unknown, Any))
+static_assert(not is_subtype_of(Unknown, Unknown))
 static_assert(not is_subtype_of(Unknown, int))
 static_assert(not is_subtype_of(int, Unknown))
 static_assert(is_subtype_of(Unknown, object))
 static_assert(not is_subtype_of(object, Unknown))
 
 static_assert(is_subtype_of(int, Unknown | int))
-static_assert(is_subtype_of(Unknown, Unknown | int))
 static_assert(is_subtype_of(Intersection[Unknown, int], int))
 static_assert(not is_subtype_of(tuple[int, int], tuple[int, Unknown]))
 ```
 
 Instances of classes that inherit `Any` are not subtypes of some other arbitrary class, because the
 `Any` they inherit from could materialize to something that is not a subclass of that class.
 
-They are also not subtypes of `Any`, because some materializations of `Any` (for example, a
-materialization into some unrelated final type) are not a super-type of any materialization of a
-specific class inheriting `Any`.
+Similarly, they are not subtypes of `Any`, because there are possible materializations that would
+not satisfy the subtype relation.
 
 They are subtypes of `object`.
 
@@ -824,7 +819,7 @@ static_assert(is_subtype_of(InheritsAny, object))
 Similar for subclass-of types:
 
 ```py
-static_assert(is_subtype_of(type[Any], type[Any]))
+static_assert(not is_subtype_of(type[Any], type[Any]))
 static_assert(not is_subtype_of(type[object], type[Any]))
 static_assert(not is_subtype_of(type[Any], type[Arbitrary]))
 static_assert(is_subtype_of(type[Any], type[object]))

crates/ty_python_semantic/src/types.rs

@@ -1165,45 +1165,93 @@ impl<'db> Type<'db> {
         }
     }
 
-    /// Return true if this type is a subtype of type `target`.
+    /// Return true if this is a type that is always fully static (has no dynamic part; represents
+    /// a single set of possible values.)
+    fn must_be_fully_static(self) -> bool {
+        match self {
+            Type::Never
+            | Type::FunctionLiteral(..)
+            | Type::BoundMethod(_)
+            | Type::WrapperDescriptor(_)
+            | Type::MethodWrapper(_)
+            | Type::DataclassDecorator(_)
+            | Type::DataclassTransformer(_)
+            | Type::ModuleLiteral(..)
+            | Type::IntLiteral(_)
+            | Type::BooleanLiteral(_)
+            | Type::StringLiteral(_)
+            | Type::LiteralString
+            | Type::BytesLiteral(_)
+            | Type::SpecialForm(_)
+            | Type::KnownInstance(_)
+            | Type::AlwaysFalsy
+            | Type::AlwaysTruthy
+            | Type::PropertyInstance(_) => true,
+            Type::ClassLiteral(_) | Type::GenericAlias(_) | Type::NominalInstance(_) => {
+                // TODO: This is wrong because the type might inherit Any
+                true
+            }
+            _ => false,
+        }
+    }
+
+    /// Return true if this type is a [subtype of] type `target`.
+    ///
+    /// For fully static types, this means that the set of objects represented by `self` is a
+    /// subset of the objects represented by `target`.
     ///
-    /// We define subtyping somewhat more broadly than [the typing spec], which defines a
-    /// strict subtyping relation that applies only to fully-static types. Our subtyping relation
-    /// is intended to be used in simplifying union and intersection types, and thus aims to uphold
-    /// the invariant that if `A` is a subtype of `B`, then `A | B` is equivalent to `B`, and `A &
-    /// B` is equivalent to `A`. Thus, we consider `Any` to be a subtype of `Any` and `object`,
-    /// for example.
+    /// For gradual types, it means that the union of all possible sets of values represented by
+    /// `self` (the "top materialization" of `self`) is a subtype of the intersection of all
+    /// possible sets of values represented by `target` (the "bottom materialization" of
+    /// `target`). In other words, for all possiblepairs of materializations `self'` and
+    /// `target'`, `self'` is always a subtype of `target'`.
     ///
-    /// The general principle we aim for is that `A` is a subtype of `B` if all materializations of
-    /// `A` are a subtype of some materialization of `B`, and all materializations of `B` are a
-    /// supertype of some materialization of `A`.
+    /// Note that this latter expansion of the subtyping relation to non-fully-static types is not
+    /// described in the typing spec, but the primary use of the subtyping relation is for
+    /// simplifying unions and intersections, and this expansion to gradual types is sound and
+    /// allows us to better simplify many unions and intersections. This definition does mean the
+    /// subtyping relation is not reflexive for non-fully-static types (e.g. `Any` is not a subtype
+    /// of `Any`).
     ///
-    /// [the typing spec]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence
+    /// [subtype of]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence
+    ///
+    /// There would be an even more general definition of subtyping for gradual types, allowing a
+    /// type `S` to be a subtype of a type `T` if the top materialization of `S` (`S+`) is a
+    /// subtype of `T+`, and the bottom materialization of `S` (`S-`) is a subtype of `T-`. This
+    /// definition is attractive in that it would restore reflexivity of subtyping for all types,
+    /// and would mean that gradual equivalence of `S` and `T` could be defined simply as `S <: T
+    /// && T <: S`. It would also be sound, in that simplifying unions or intersections according
+    /// to this definition of subtyping would still result in an equivalent type.
+    ///
+    /// Unfortunately using this definition would break transitivity of subtyping when
+    /// both nominal and structural types are involved, because Liskov enforcement for nominal
+    /// types is based on assignability, so we can have class `A` with method `def meth() -> Any`
+    /// and a subclass `B(A)` with method `def meth() -> int`. In this case, `A` would be a subtype
+    /// of a protocol `P` with method `def meth() -> str`, but `B` would not be a subtype of `P`,
+    /// and yet `B` is (by nominal subtyping) a subtype of `A`, so we would have `B <: A` and `A <:
+    /// P`, but not `B <: P`. Losing transitivity of subtyping is not tenable (it makes union and
+    /// intersection simplification dependent on the order in which elements are added), so we do
+    /// not use this more general definition of subtyping.
     pub(crate) fn is_subtype_of(self, db: &'db dyn Db, target: Type<'db>) -> bool {
         self.has_relation_to(db, target, TypeRelation::Subtyping)
     }
 
     /// Return true if this type is [assignable to] type `target`.
     ///
-    /// In contrast to subtyping, `A` is assignable to `B` if there are any possible
-    /// materializations `A'` and `B'` such that `A'` is a subtype of `B'`.
-    ///
-    /// TODO: We may need to add a restriction that this "possible materialization" cannot be
-    /// `Never`.
-    ///
     /// [assignable to]: https://typing.python.org/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation
     pub(crate) fn is_assignable_to(self, db: &'db dyn Db, target: Type<'db>) -> bool {
         self.has_relation_to(db, target, TypeRelation::Assignability)
     }
 
     fn has_relation_to(self, db: &'db dyn Db, target: Type<'db>, relation: TypeRelation) -> bool {
-        // If two types are the same type, they are both subtypes of each other and assignable to
-        // each other.
-        if self == target {
+        // If two types that must be fully static are the same type, they are both subtypes of
+        // each other and assignable to each other.
+        if self.must_be_fully_static() && target.must_be_fully_static() && self == target {
             return true;
         }
-        // If two types are equivalent, they are subtypes of and assignable to each other.
-        if self.is_equivalent_to(db, target) {
+        // If two types are equivalent, they are assignable to each other. (Equivalence does
+        // not imply subtyping, since it may be gradual equivalence.)
+        if relation.is_assignability() && self.is_equivalent_to(db, target) {
             return true;
         }
 
@@ -1215,11 +1263,9 @@ impl<'db> Type<'db> {
             // It is a subtype of all other types.
             (Type::Never, _) => true,
 
-            // The dynamic type is always assignable to and a subtype of itself.
-            (Type::Dynamic(_), Type::Dynamic(_)) => true,
-
-            // The dynamic type is always assignable to or from any other type.
-            (Type::Dynamic(_), _) | (_, Type::Dynamic(_)) if relation.is_assignability() => true,
+            // Dynamic is only a subtype of `object` and only a supertype of `Never`; both were
+            // handled above. It's always assignable, though.
+            (Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => relation.is_assignability(),
 
             // In general, a TypeVar `T` is not a subtype of a type `S` unless one of the two conditions is satisfied:
             // 1. `T` is a bound TypeVar and `T`'s upper bound is a subtype of `S`.
@@ -1319,10 +1365,6 @@ impl<'db> Type<'db> {
             // be specialized to `Never`.)
             (_, Type::TypeVar(_)) => false,
 
-            // Other than `object` or `Never` or unions or intersections, all handled above,
-            // the dynamic type is never a subtype or supertype of any other type.
-            (Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => false,
-
             // Note that the definition of `Type::AlwaysFalsy` depends on the return value of `__bool__`.
             // If `__bool__` always returns True or False, it can be treated as a subtype of `AlwaysTruthy` or `AlwaysFalsy`, respectively.
             (left, Type::AlwaysFalsy) => left.bool(db).is_always_false(),

crates/ty_python_semantic/src/types/builder.rs

@@ -369,7 +369,9 @@ impl<'db> UnionBuilder<'db> {
                         return;
                     }
 
-                    if ty.is_subtype_of(self.db, element_type) {
+                    if ty.is_equivalent_to(self.db, element_type)
+                        || ty.is_subtype_of(self.db, element_type)
+                    {
                         return;
                     } else if element_type.is_subtype_of(self.db, ty) {
                         to_remove.push(index);
@@ -671,7 +673,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_equivalent_to(db, new_positive)
+                    {
                         return;
                     }
                     // same rule, reverse order
@@ -766,7 +770,9 @@ impl<'db> InnerIntersectionBuilder<'db> {
                 let mut to_remove = SmallVec::<[usize; 1]>::new();
                 for (index, existing_negative) in self.negative.iter().enumerate() {
                     // ~S & ~T = ~T    if S <: T
-                    if existing_negative.is_subtype_of(db, new_negative) {
+                    if existing_negative.is_subtype_of(db, new_negative)
+                        || existing_negative.is_equivalent_to(db, new_negative)
+                    {
                         to_remove.push(index);
                     }
                     // same rule, reverse order

crates/ty_python_semantic/src/types/property_tests.rs

@@ -50,9 +50,19 @@ macro_rules! type_property_test {
             $property
         }
     };
+    ($test_name:ident, $db:ident, forall fully_static_types $($types:ident),+ . $property:expr) => {
+        #[quickcheck_macros::quickcheck]
+        #[ignore]
+        fn $test_name($($types: crate::types::property_tests::type_generation::FullyStaticTy),+) -> bool {
+            let $db = &crate::types::property_tests::setup::get_cached_db();
+            $(let $types = $types.into_type($db);)+
+
+            $property
+        }
+    };
     // A property test with a logical implication.
-    ($name:ident, $db:ident, forall types $($types:ident),+ . $premise:expr => $conclusion:expr) => {
-        type_property_test!($name, $db, forall types $($types),+ . !($premise) || ($conclusion));
+    ($name:ident, $db:ident, forall $typekind:ident $($types:ident),+ . $premise:expr => $conclusion:expr) => {
+        type_property_test!($name, $db, forall $typekind $($types),+ . !($premise) || ($conclusion));
     };
 }
 
@@ -90,12 +100,6 @@ mod stable {
         forall types s, t. s.is_subtype_of(db, t) && t.is_subtype_of(db, s) => s.is_equivalent_to(db, t)
     );
 
-    // Equivalence implies subtyping.
-    type_property_test!(
-        equivalence_implies_subtype, db,
-        forall types s, t. s.is_equivalent_to(db, t) => s.is_subtype_of(db, t) && t.is_subtype_of(db, s)
-    );
-
     // `T` is not disjoint from itself, unless `T` is `Never`.
     type_property_test!(
         disjoint_from_is_irreflexive, db,
@@ -169,16 +173,16 @@ mod stable {
         forall types s, t. s.is_assignable_to(db, union(db, [s, t])) && t.is_assignable_to(db, union(db, [s, t]))
     );
 
-    // A type `T` is a subtype of itself.
+    // A fully static type `T` is a subtype of itself.
     type_property_test!(
-        subtype_of_is_reflexive, db,
-        forall types t. t.is_subtype_of(db, t)
+        subtype_of_is_reflexive_for_fully_static_types, db,
+        forall fully_static_types t. t.is_subtype_of(db, t)
     );
 
-    // For any two types, each type in the pair must be a subtype of their union.
+    // For any two fully static types, each type in the pair must be a subtype of their union.
     type_property_test!(
-        all_type_pairs_are_subtype_of_their_union, db,
-        forall types s, t. s.is_subtype_of(db, union(db, [s, t])) && t.is_subtype_of(db, union(db, [s, t]))
+        all_fully_static_type_pairs_are_subtype_of_their_union, db,
+        forall fully_static_types s, t. s.is_subtype_of(db, union(db, [s, t])) && t.is_subtype_of(db, union(db, [s, t]))
     );
 }