Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[red-knot] Document public symbol type inference #15766

Merged
merged 1 commit into from
Jan 27, 2025
Merged

[red-knot] Document public symbol type inference #15766

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
158 changes: 97 additions & 61 deletions crates/red_knot_python_semantic/resources/mdtest/boundness_declaredness/public.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# 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]`).
Expand Down Expand Up @@ -34,20 +34,26 @@ In particular, we should raise errors in the "possibly-undeclared-and-unbound" a
### Declared and bound

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
x: int = 1
from typing import Any

# error: [invalid-assignment]
y: str = 2
def any() -> Any: ...

a: int = 1
b: str = 2 # error: [invalid-assignment]
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
reveal_type(d) # revealed: int
```

### Declared and possibly unbound
Expand All @@ -56,21 +62,30 @@ 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
# error: [invalid-assignment]
y = 2
a = 1
b = 2 # error: [invalid-assignment]
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
reveal_type(d) # revealed: int
```

### Declared and unbound
Expand All @@ -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.

```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
Expand All @@ -98,58 +117,61 @@ inferred types:
```py path=mod.py
from typing import Any

def any() -> Any: ...
def flag() -> bool: ...

x = 1
y = 2
z = 3
a = 1
b = 2
c = 3
d = any()
if flag():
x: int
y: Any
# error: [invalid-declaration]
z: str
a: int
b: Any
c: str # error: [invalid-declaration]
d: int
```

```py
from mod import x, y, z
from mod import a, b, c, d

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
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]
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
Expand All @@ -161,36 +183,46 @@ 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

### 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
x = 1
from knot_extensions import Unknown

# Undeclared:
a = 1

# Declared with `Unknown`:
b: Unknown = 1
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think something that is noteworthy here is that the entire purpose of Unknown (as distinct from Any) is to distinguish a dynamic type that originates from an explicit annotation vs one that originates from lack of annotation. So the whole idea of "declared with Unknown" is a contradiction. We have made it possible by introducing knot_extensions.Unknown, but perhaps that is just confusing and was a mistake? It should really only be used in tests, but I would guess that in most cases we could structure the test so as to generate an Unknown type via lack-of-annotation instead (e.g. an un-annotated function parameter).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually I just realized that "declared with Unknown" is not a contradiction; it could occur anytime someone annotates with a name we can't resolve, or an invalid type expression.

Still not totally clear to me whether tests for this case are better written using knot_extensions.Unknown (which is clear and explicit, but not "realistic") or using an actual unknown name (which then requires suppressing the unknown-name diagnostic.) I can see good arguments both ways, so no strong feelings.

```

```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
Comment on lines +221 to +222
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This behavior is the main thing I wanted to document.


# All external modifications of `x` are allowed:
x = None
# All external modifications of `a` are allowed:
a = None
```

### Undeclared and possibly unbound
Expand All @@ -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.

```py path=mod.py
from knot_extensions import Unknown

def flag() -> bool: ...

if flag:
x = 1
a = 1
b: Unknown = 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, 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:
x = None
# All external modifications of `a` are allowed:
a = None
```

### Undeclared and unbound
Expand All @@ -222,15 +258,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
```
Loading