From a3d730bc7cf4434ca37bbd7254c2b11b2732ace2 Mon Sep 17 00:00:00 2001 From: David Peter Date: Fri, 24 Jan 2025 14:09:30 +0100 Subject: [PATCH] [red-knot] Use `T_declared | T_inferred` for declared public symbols --- .../resources/mdtest/annotations/any.md | 4 +- .../annotations/unsupported_special_forms.md | 2 +- .../mdtest/assignment/annotations.md | 8 +- .../resources/mdtest/attributes.md | 6 +- .../mdtest/boundness_declaredness/public.md | 154 +++++++++++------- .../mdtest/type_qualifiers/classvar.md | 3 +- crates/red_knot_python_semantic/src/types.rs | 82 ++++++++-- 7 files changed, 173 insertions(+), 86 deletions(-) diff --git a/crates/red_knot_python_semantic/resources/mdtest/annotations/any.md b/crates/red_knot_python_semantic/resources/mdtest/annotations/any.md index b5b43a8412bac6..9fb90a532ccde6 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/annotations/any.md +++ b/crates/red_knot_python_semantic/resources/mdtest/annotations/any.md @@ -11,7 +11,7 @@ x: Any = 1 x = "foo" def f(): - reveal_type(x) # revealed: Any + reveal_type(x) # revealed: Any | Literal["foo"] ``` ## Aliased to a different name @@ -25,7 +25,7 @@ x: RenamedAny = 1 x = "foo" def f(): - reveal_type(x) # revealed: Any + reveal_type(x) # revealed: Any | Literal["foo"] ``` ## Shadowed class diff --git a/crates/red_knot_python_semantic/resources/mdtest/annotations/unsupported_special_forms.md b/crates/red_knot_python_semantic/resources/mdtest/annotations/unsupported_special_forms.md index 37d9dfb7d43c3b..7aedd71ff53e80 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/annotations/unsupported_special_forms.md +++ b/crates/red_knot_python_semantic/resources/mdtest/annotations/unsupported_special_forms.md @@ -18,7 +18,7 @@ def f(*args: Unpack[Ts]) -> tuple[Unpack[Ts]]: # TODO: should understand the annotation reveal_type(args) # revealed: tuple - reveal_type(Alias) # revealed: @Todo(Unsupported or invalid type in a type expression) + reveal_type(Alias) # revealed: @Todo(Unsupported or invalid type in a type expression) | Literal[int] def g() -> TypeGuard[int]: ... def h() -> TypeIs[int]: ... diff --git a/crates/red_knot_python_semantic/resources/mdtest/assignment/annotations.md b/crates/red_knot_python_semantic/resources/mdtest/assignment/annotations.md index c1fee047feab60..93cdde6705089f 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/assignment/annotations.md +++ b/crates/red_knot_python_semantic/resources/mdtest/assignment/annotations.md @@ -49,12 +49,12 @@ reveal_type(c) # revealed: tuple[str, int] reveal_type(d) # revealed: tuple[tuple[str, str], tuple[int, int]] # TODO: homogeneous tuples, PEP-646 tuples -reveal_type(e) # revealed: @Todo(full tuple[...] support) -reveal_type(f) # revealed: @Todo(full tuple[...] support) -reveal_type(g) # revealed: @Todo(full tuple[...] support) +reveal_type(e) # revealed: @Todo(full tuple[...] support) | tuple[()] +reveal_type(f) # revealed: @Todo(full tuple[...] support) | tuple[Literal["42"], Literal[b"42"]] +reveal_type(g) # revealed: @Todo(full tuple[...] support) | tuple[Literal["42"], Literal[b"42"]] # TODO: support more kinds of type expressions in annotations -reveal_type(h) # revealed: @Todo(full tuple[...] support) +reveal_type(h) # revealed: @Todo(full tuple[...] support) | tuple[list, list] reveal_type(i) # revealed: tuple[str | int, str | int] reveal_type(j) # revealed: tuple[str | int] diff --git a/crates/red_knot_python_semantic/resources/mdtest/attributes.md b/crates/red_knot_python_semantic/resources/mdtest/attributes.md index 63cc31d0dbc0f2..61436d971ba88f 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/attributes.md +++ b/crates/red_knot_python_semantic/resources/mdtest/attributes.md @@ -175,16 +175,14 @@ class C: reveal_type(C.pure_class_variable1) # revealed: str -# TODO: Should be `Unknown | Literal[1]`. -reveal_type(C.pure_class_variable2) # revealed: Unknown +reveal_type(C.pure_class_variable2) # revealed: Unknown | Literal[1] c_instance = C() # It is okay to access a pure class variable on an instance. reveal_type(c_instance.pure_class_variable1) # revealed: str -# TODO: Should be `Unknown | Literal[1]`. -reveal_type(c_instance.pure_class_variable2) # revealed: Unknown +reveal_type(c_instance.pure_class_variable2) # revealed: Unknown | Literal[1] # error: [invalid-attribute-access] "Cannot assign to ClassVar `pure_class_variable1` from an instance of type `C`" c_instance.pure_class_variable1 = "value set on instance" diff --git a/crates/red_knot_python_semantic/resources/mdtest/boundness_declaredness/public.md b/crates/red_knot_python_semantic/resources/mdtest/boundness_declaredness/public.md index 55c4e7e9c7dda8..32cfc9de5238bf 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/boundness_declaredness/public.md +++ b/crates/red_knot_python_semantic/resources/mdtest/boundness_declaredness/public.md @@ -1,9 +1,13 @@ # Boundness and declaredness: public uses -This document demonstrates how type-inference and diagnostics works for *public* uses of a symbol, +This document demonstrates how type-inference and diagnostics work for *public* uses of a symbol, that is, a use of a symbol from another scope. If a symbol has a declared type in its local scope (e.g. `int`), we use that as the symbol's "public type" (the type of the symbol from the perspective -of other scopes) even if there is a more precise local inferred type for the symbol (`Literal[1]`). +of other scopes). If there is an inferred type in addition (i.e. if we also see bindings for this +symbol, not just declarations), we build the union of the declared and inferred types. For fully- +static types, the inferred type must be a subtype of the declared type (otherwise we would issue +diagnostics). For dynamic types, however, this can lead to more precise types with lower bounds +given by the inferred type (e.g. `Any | Literal[1]` for a symbol defined as `x: Any = 1`). If a symbol has no declared type, we use the union of `Unknown` with the inferred type as the public type. If there is no declaration, then the symbol can be reassigned to any type from another scope; @@ -17,11 +21,11 @@ this behavior is questionable and might change in the future. See the TODOs in ` In particular, we should raise errors in the "possibly-undeclared-and-unbound" as well as the "undeclared-and-possibly-unbound" cases (marked with a "?"). -| **Public type** | declared | possibly-undeclared | undeclared | -| ---------------- | ------------ | -------------------------- | ----------------------- | -| bound | `T_declared` | `T_declared \| T_inferred` | `Unknown \| T_inferred` | -| possibly-unbound | `T_declared` | `T_declared \| T_inferred` | `Unknown \| T_inferred` | -| unbound | `T_declared` | `T_declared` | `Unknown` | +| **Public type** | declared | possibly-undeclared | undeclared | +| ---------------- | -------------------------- | -------------------------- | ------------------ | +| bound | `T_decl \| T_decl & T_inf` | `T_decl \| T_decl & T_inf` | `Unknown \| T_inf` | +| possibly-unbound | `T_decl \| T_decl & T_inf` | `T_decl \| T_decl & T_inf` | `Unknown \| T_inf` | +| unbound | `T_decl` | `T_decl` | `Unknown` | | **Diagnostic** | declared | possibly-undeclared | undeclared | | ---------------- | -------- | ------------------------- | ------------------- | @@ -37,17 +41,27 @@ If a symbol has a declared type (`int`), we use that even if there is a more pre (`Literal[1]`), or a conflicting inferred type (`Literal[2]`): ```py path=mod.py -x: int = 1 +from typing import Any + +def any() -> Any: ... + +a: int = 1 # error: [invalid-assignment] -y: str = 2 +b: str = 2 + +c: Any = 3 + +d: int = any() ``` ```py -from mod import x, y +from mod import a, b, c, d -reveal_type(x) # revealed: int -reveal_type(y) # revealed: str +reveal_type(a) # revealed: int +reveal_type(b) # revealed: str +reveal_type(c) # revealed: Any | Literal[3] +reveal_type(d) # revealed: int ``` ### Declared and possibly unbound @@ -56,21 +70,31 @@ If a symbol is declared and *possibly* unbound, we trust that other module and u without raising an error. ```py path=mod.py +from typing import Any + +def any() -> Any: ... def flag() -> bool: ... -x: int -y: str +a: int +b: str +c: Any +d: int + if flag: - x = 1 + a = 1 # error: [invalid-assignment] - y = 2 + b = 2 + c = 3 + d = any() ``` ```py -from mod import x, y +from mod import a, b, c, d -reveal_type(x) # revealed: int -reveal_type(y) # revealed: str +reveal_type(a) # revealed: int +reveal_type(b) # revealed: str +reveal_type(c) # revealed: Any | Literal[3] +reveal_type(d) # revealed: int ``` ### Declared and unbound @@ -79,13 +103,17 @@ Similarly, if a symbol is declared but unbound, we do not raise an error. We tru is available somehow and simply use the declared type. ```py path=mod.py -x: int +from typing import Any + +a: int +b: Any ``` ```py -from mod import x +from mod import a, b -reveal_type(x) # revealed: int +reveal_type(a) # revealed: int +reveal_type(b) # revealed: Any ``` ## Possibly undeclared @@ -100,56 +128,56 @@ from typing import Any def flag() -> bool: ... -x = 1 -y = 2 -z = 3 +a = 1 +b = 2 +c = 3 if flag(): - x: int - y: Any + a: int + b: Any # error: [invalid-declaration] - z: str + c: str ``` ```py -from mod import x, y, z +from mod import a, b, c -reveal_type(x) # revealed: int -reveal_type(y) # revealed: Literal[2] | Any -reveal_type(z) # revealed: Literal[3] | Unknown +reveal_type(a) # revealed: int +reveal_type(b) # revealed: Literal[2] | Any +reveal_type(c) # revealed: Literal[3] | Unknown -# External modifications of `x` that violate the declared type are not allowed: +# External modifications of `a` that violate the declared type are not allowed: # error: [invalid-assignment] -x = None +a = None ``` ### Possibly undeclared and possibly unbound If a symbol is possibly undeclared and possibly unbound, we also use the union of the declared and inferred types. This case is interesting because the "possibly declared" definition might not be the -same as the "possibly bound" definition (symbol `y`). Note that we raise a `possibly-unbound-import` -error for both `x` and `y`: +same as the "possibly bound" definition (symbol `b`). Note that we raise a `possibly-unbound-import` +error for both `a` and `b`: ```py path=mod.py def flag() -> bool: ... if flag(): - x: Any = 1 - y = 2 + a: Any = 1 + b = 2 else: - y: str + b: str ``` ```py # error: [possibly-unbound-import] # error: [possibly-unbound-import] -from mod import x, y +from mod import a, b -reveal_type(x) # revealed: Literal[1] | Any -reveal_type(y) # revealed: Literal[2] | str +reveal_type(a) # revealed: Literal[1] | Any +reveal_type(b) # revealed: Literal[2] | str -# External modifications of `y` that violate the declared type are not allowed: +# External modifications of `b` that violate the declared type are not allowed: # error: [invalid-assignment] -y = None +b = None ``` ### Possibly undeclared and unbound @@ -161,19 +189,19 @@ seems inconsistent when compared to the case just above. def flag() -> bool: ... if flag(): - x: int + a: int ``` ```py # TODO: this should raise an error. Once we fix this, update the section description and the table # on top of this document. -from mod import x +from mod import a -reveal_type(x) # revealed: int +reveal_type(a) # revealed: int -# External modifications to `x` that violate the declared type are not allowed: +# External modifications to `a` that violate the declared type are not allowed: # error: [invalid-assignment] -x = None +a = None ``` ## Undeclared @@ -181,16 +209,16 @@ x = None ### Undeclared but bound ```py path=mod.py -x = 1 +a = 1 ``` ```py -from mod import x +from mod import a -reveal_type(x) # revealed: Unknown | Literal[1] +reveal_type(a) # revealed: Unknown | Literal[1] -# All external modifications of `x` are allowed: -x = None +# All external modifications of `a` are allowed: +a = None ``` ### Undeclared and possibly unbound @@ -202,18 +230,18 @@ inconsistent when compared to the "possibly-undeclared-and-possibly-unbound" cas def flag() -> bool: ... if flag: - x = 1 + a = 1 ``` ```py # TODO: this should raise an error. Once we fix this, update the section description and the table # on top of this document. -from mod import x +from mod import a -reveal_type(x) # revealed: Unknown | Literal[1] +reveal_type(a) # revealed: Unknown | Literal[1] -# All external modifications of `x` are allowed: -x = None +# All external modifications of `a` are allowed: +a = None ``` ### Undeclared and unbound @@ -222,15 +250,15 @@ If a symbol is undeclared *and* unbound, we infer `Unknown` and raise an error. ```py path=mod.py if False: - x: int = 1 + a: int = 1 ``` ```py # error: [unresolved-import] -from mod import x +from mod import a -reveal_type(x) # revealed: Unknown +reveal_type(a) # revealed: Unknown # Modifications allowed in this case: -x = None +a = None ``` diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_qualifiers/classvar.md b/crates/red_knot_python_semantic/resources/mdtest/type_qualifiers/classvar.md index 26060e685d3bbf..cf80afaa11183a 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/type_qualifiers/classvar.md +++ b/crates/red_knot_python_semantic/resources/mdtest/type_qualifiers/classvar.md @@ -21,8 +21,7 @@ class C: reveal_type(C.a) # revealed: int reveal_type(C.b) # revealed: int reveal_type(C.c) # revealed: int -# TODO: should be Unknown | Literal[1] -reveal_type(C.d) # revealed: Unknown +reveal_type(C.d) # revealed: Unknown | Literal[1] reveal_type(C.e) # revealed: int c = C() diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 69940e4a9d78f9..d9cc932ba8be2b 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -103,6 +103,54 @@ fn widen_type_for_undeclared_public_symbol<'db>( } } +/// Computes a possibly more precise public type for a (possibly) declared symbol where +/// we also have an inferred type from visible bindings. +/// +/// Below, we build the type `declared_ty | declared_ty & inferred_ty`. This represents +/// the fact that we want to return a type that is no larger than and no smaller than +/// `declared_ty`. If `declared_ty` is a fully static type, this means that we will +/// simply return `declared_ty`. But if `declared_ty` is an arbitrary gradual type, this +/// can make the public type more specific by including information about `inferred_ty`. +/// +/// We have a special handling for the following cases, both for performance reasons +/// and to construct the easiest possible representation of a type: +/// +/// ```txt +/// inferred_ty = Any/Unknown +/// +/// => declared_ty | declared_ty & Any = declared_ty +/// +/// declared_ty = Any/Unknown +/// +/// => Any | Any & inferred_ty = Any | inferred_ty +/// ``` +fn widen_type_for_declared_public_symbol<'db>( + db: &'db dyn Db, + declared_ty: Type<'db>, + inferred: &Symbol<'db>, +) -> Type<'db> { + match inferred.ignore_possibly_unbound() { + Some(inferred_ty) => { + if inferred_ty.is_dynamic() { + declared_ty + } else if declared_ty.is_dynamic() { + UnionType::from_elements(db, [declared_ty, inferred_ty]) + } else if declared_ty.is_fully_static(db) { + declared_ty + } else { + IntersectionBuilder::new(db) + .add_positive(UnionType::from_elements( + db, + [declared_ty, inferred_ty].iter().copied(), + )) + .add_positive(declared_ty) + .build() + } + } + None => declared_ty, + } +} + /// Infer the public type of a symbol (its type as seen from outside its scope). fn symbol<'db>(db: &'db dyn Db, scope: ScopeId<'db>, name: &str) -> Symbol<'db> { #[salsa::tracked] @@ -122,14 +170,17 @@ fn symbol<'db>(db: &'db dyn Db, scope: ScopeId<'db>, name: &str) -> Symbol<'db> let is_final = declared.as_ref().is_ok_and(SymbolAndQualifiers::is_final); let declared = declared.map(|SymbolAndQualifiers(symbol, _)| symbol); + let bindings = use_def.public_bindings(symbol_id); + let inferred = symbol_from_bindings(db, bindings); + match declared { - // Symbol is declared, trust the declared type - Ok(symbol @ Symbol::Type(_, Boundness::Bound)) => symbol, + // Symbol is declared + Ok(Symbol::Type(declared_ty, Boundness::Bound)) => Symbol::Type( + widen_type_for_declared_public_symbol(db, declared_ty, &inferred), + Boundness::Bound, + ), // Symbol is possibly declared Ok(Symbol::Type(declared_ty, Boundness::PossiblyUnbound)) => { - let bindings = use_def.public_bindings(symbol_id); - let inferred = symbol_from_bindings(db, bindings); - match inferred { // Symbol is possibly undeclared and definitely unbound Symbol::Unbound => { @@ -646,6 +697,10 @@ impl<'db> Type<'db> { matches!(self, Type::Dynamic(DynamicType::Todo(_))) } + pub const fn is_dynamic(&self) -> bool { + matches!(self, Type::Dynamic(_)) + } + pub const fn class_literal(class: Class<'db>) -> Self { Self::ClassLiteral(ClassLiteralType { class }) } @@ -4125,8 +4180,12 @@ impl<'db> Class<'db> { let use_def = use_def_map(db, body_scope); let declarations = use_def.public_declarations(symbol_id); + let declared = symbol_from_declarations(db, declarations); - match symbol_from_declarations(db, declarations) { + let bindings = use_def.public_bindings(symbol_id); + let inferred = symbol_from_bindings(db, bindings); + + match declared { Ok(SymbolAndQualifiers(Symbol::Type(declared_ty, _), qualifiers)) => { if let Some(function) = declared_ty.into_function_literal() { // TODO: Eventually, we are going to process all decorators correctly. This is @@ -4138,13 +4197,16 @@ impl<'db> Class<'db> { todo_type!("bound method").into() } } else { - SymbolAndQualifiers(Symbol::Type(declared_ty, Boundness::Bound), qualifiers) + SymbolAndQualifiers( + Symbol::Type( + widen_type_for_declared_public_symbol(db, declared_ty, &inferred), + Boundness::Bound, + ), + qualifiers, + ) } } Ok(symbol @ SymbolAndQualifiers(Symbol::Unbound, qualifiers)) => { - let bindings = use_def.public_bindings(symbol_id); - let inferred = symbol_from_bindings(db, bindings); - SymbolAndQualifiers( widen_type_for_undeclared_public_symbol(db, inferred, symbol.is_final()), qualifiers,