[red-knot] Document public symbol type inferece (#15766)

## Summary

Adds a slightly more comprehensive documentation of our behavior
regarding type inference for public uses of symbols. In particular:

- What public type do we infer for `x: int = any()`?
- What public type do we infer for `x: Unknown = 1`?
This commit is contained in:
David Peter 2025-01-27 10:52:13 +01:00 committed by GitHub
parent 3a08570a68
commit 2ef94e5f3e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -1,6 +1,6 @@
# Boundness and declaredness: public uses # 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 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 (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) even if there is a more precise local inferred type for the symbol (`Literal[1]`).
@ -34,20 +34,26 @@ In particular, we should raise errors in the "possibly-undeclared-and-unbound" a
### Declared and bound ### Declared and bound
If a symbol has a declared type (`int`), we use that even if there is a more precise inferred type If a symbol has a declared type (`int`), we use that even if there is a more precise inferred type
(`Literal[1]`), or a conflicting inferred type (`Literal[2]`): (`Literal[1]`), or a conflicting inferred type (`str` vs. `Literal[2]` below):
```py path=mod.py ```py path=mod.py
x: int = 1 from typing import Any
# error: [invalid-assignment] def any() -> Any: ...
y: str = 2
a: int = 1
b: str = 2 # error: [invalid-assignment]
c: Any = 3
d: int = any()
``` ```
```py ```py
from mod import x, y from mod import a, b, c, d
reveal_type(x) # revealed: int reveal_type(a) # revealed: int
reveal_type(y) # revealed: str reveal_type(b) # revealed: str
reveal_type(c) # revealed: Any
reveal_type(d) # revealed: int
``` ```
### Declared and possibly unbound ### Declared and possibly unbound
@ -56,21 +62,30 @@ If a symbol is declared and *possibly* unbound, we trust that other module and u
without raising an error. without raising an error.
```py path=mod.py ```py path=mod.py
from typing import Any
def any() -> Any: ...
def flag() -> bool: ... def flag() -> bool: ...
x: int a: int
y: str b: str
c: Any
d: int
if flag: if flag:
x = 1 a = 1
# error: [invalid-assignment] b = 2 # error: [invalid-assignment]
y = 2 c = 3
d = any()
``` ```
```py ```py
from mod import x, y from mod import a, b, c, d
reveal_type(x) # revealed: int reveal_type(a) # revealed: int
reveal_type(y) # revealed: str reveal_type(b) # revealed: str
reveal_type(c) # revealed: Any
reveal_type(d) # revealed: int
``` ```
### Declared and unbound ### Declared and unbound
@ -79,13 +94,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. is available somehow and simply use the declared type.
```py path=mod.py ```py path=mod.py
x: int from typing import Any
a: int
b: Any
``` ```
```py ```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 ## Possibly undeclared
@ -98,58 +117,61 @@ inferred types:
```py path=mod.py ```py path=mod.py
from typing import Any from typing import Any
def any() -> Any: ...
def flag() -> bool: ... def flag() -> bool: ...
x = 1 a = 1
y = 2 b = 2
z = 3 c = 3
d = any()
if flag(): if flag():
x: int a: int
y: Any b: Any
# error: [invalid-declaration] c: str # error: [invalid-declaration]
z: str d: int
``` ```
```py ```py
from mod import x, y, z from mod import a, b, c, d
reveal_type(x) # revealed: int reveal_type(a) # revealed: int
reveal_type(y) # revealed: Literal[2] | Any reveal_type(b) # revealed: Literal[2] | Any
reveal_type(z) # revealed: Literal[3] | Unknown reveal_type(c) # revealed: Literal[3] | Unknown
reveal_type(d) # revealed: Any | int
# 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] # error: [invalid-assignment]
x = None a = None
``` ```
### Possibly undeclared and possibly unbound ### Possibly undeclared and possibly unbound
If a symbol is possibly undeclared and possibly unbound, we also use the union of the declared and 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 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` same as the "possibly bound" definition (symbol `b`). Note that we raise a `possibly-unbound-import`
error for both `x` and `y`: error for both `a` and `b`:
```py path=mod.py ```py path=mod.py
def flag() -> bool: ... def flag() -> bool: ...
if flag(): if flag():
x: Any = 1 a: Any = 1
y = 2 b = 2
else: else:
y: str b: str
``` ```
```py ```py
# error: [possibly-unbound-import] # error: [possibly-unbound-import]
# 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(a) # revealed: Literal[1] | Any
reveal_type(y) # revealed: Literal[2] | str 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] # error: [invalid-assignment]
y = None b = None
``` ```
### Possibly undeclared and unbound ### Possibly undeclared and unbound
@ -161,36 +183,46 @@ seems inconsistent when compared to the case just above.
def flag() -> bool: ... def flag() -> bool: ...
if flag(): if flag():
x: int a: int
``` ```
```py ```py
# TODO: this should raise an error. Once we fix this, update the section description and the table # TODO: this should raise an error. Once we fix this, update the section description and the table
# on top of this document. # 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] # error: [invalid-assignment]
x = None a = None
``` ```
## Undeclared ## Undeclared
### Undeclared but bound ### Undeclared but bound
If a symbols is undeclared, we use the union of `Unknown` with the inferred type. Note that we treat
symbols that are undeclared differently from symbols that are explicitly declared as `Unknown`:
```py path=mod.py ```py path=mod.py
x = 1 from knot_extensions import Unknown
# Undeclared:
a = 1
# Declared with `Unknown`:
b: Unknown = 1
``` ```
```py ```py
from mod import x from mod import a, b
reveal_type(x) # revealed: Unknown | Literal[1] reveal_type(a) # revealed: Unknown | Literal[1]
reveal_type(b) # revealed: Unknown
# All external modifications of `x` are allowed: # All external modifications of `a` are allowed:
x = None a = None
``` ```
### Undeclared and possibly unbound ### Undeclared and possibly unbound
@ -199,21 +231,25 @@ If a symbol is undeclared and *possibly* unbound, we currently do not raise an e
inconsistent when compared to the "possibly-undeclared-and-possibly-unbound" case. inconsistent when compared to the "possibly-undeclared-and-possibly-unbound" case.
```py path=mod.py ```py path=mod.py
from knot_extensions import Unknown
def flag() -> bool: ... def flag() -> bool: ...
if flag: if flag:
x = 1 a = 1
b: Unknown = 1
``` ```
```py ```py
# TODO: this should raise an error. Once we fix this, update the section description and the table # TODO: this should raise an error. Once we fix this, update the section description and the table
# on top of this document. # on top of this document.
from mod import x from mod import a, b
reveal_type(x) # revealed: Unknown | Literal[1] reveal_type(a) # revealed: Unknown | Literal[1]
reveal_type(b) # revealed: Unknown
# All external modifications of `x` are allowed: # All external modifications of `a` are allowed:
x = None a = None
``` ```
### Undeclared and unbound ### Undeclared and unbound
@ -222,15 +258,15 @@ If a symbol is undeclared *and* unbound, we infer `Unknown` and raise an error.
```py path=mod.py ```py path=mod.py
if False: if False:
x: int = 1 a: int = 1
``` ```
```py ```py
# error: [unresolved-import] # 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: # Modifications allowed in this case:
x = None a = None
``` ```