Files
ruff/crates/red_knot_python_semantic/resources/mdtest/binary/integers.md
Carl Meyer e2a30b71f4 [red-knot] revert change to emit fewer division by zero errors (#13801)
This reverts https://github.com/astral-sh/ruff/pull/13799, and restores
the previous behavior, which I think was the most pragmatic and useful
version of the divide-by-zero error, if we will emit it at all.

In general, a type checker _does_ emit diagnostics when it can detect
something that will definitely be a problem for some inhabitants of a
type, but not others. For example, `x.foo` if `x` is typed as `object`
is a type error, even though some inhabitants of the type `object` will
have a `foo` attribute! The correct fix is to make your type annotations
more precise, so that `x` is assigned a type which definitely has the
`foo` attribute.

If we will emit it divide-by-zero errors, it should follow the same
logic. Dividing an inhabitant of the type `int` by zero may not emit an
error, if the inhabitant is an instance of a subclass of `builtins.int`
that overrides division. But it may emit an error (more likely it will).
If you don't want the diagnostic, you can clarify your type annotations
to require an instance of your safe subclass.

Because the Python type system doesn't have the ability to explicitly
reflect the fact that divide-by-zero is an error in type annotations
(e.g. for `int.__truediv__`), or conversely to declare a type as safe
from divide-by-zero, or include a "nonzero integer" type which it is
always safe to divide by, the analogy doesn't fully apply. You can't
explicitly mark your subclass of `int` as safe from divide-by-zero, we
just semi-arbitrarily choose to silence the diagnostic for subclasses,
to avoid false positives.

Also, if we fully followed the above logic, we'd have to error on every
`int / int` because the RHS `int` might be zero! But this would likely
cause too many false positives, because of the lack of a "nonzero
integer" type.

So this is just a pragmatic choice to emit the diagnostic when it is
very likely to be an error. It's unclear how useful this diagnostic is
in practice, but this version of it is at least very unlikely to cause
harm.
2024-10-17 20:17:22 +00:00

1.9 KiB

Binary operations on integers

Basic Arithmetic

a = 2 + 1
b = a - 4
c = a * b
d = c // 3
e = c / 3
f = 5 % 3

reveal_type(a)  # revealed: Literal[3]
reveal_type(b)  # revealed: Literal[-1]
reveal_type(c)  # revealed: Literal[-3]
reveal_type(d)  # revealed: Literal[-1]
reveal_type(e)  # revealed: float
reveal_type(f)  # revealed: Literal[2]

Division by Zero

This error is really outside the current Python type system, because e.g. int.__truediv__ and friends are not annotated to indicate that it's an error, and we don't even have a facility to permit such an annotation. So arguably divide-by-zero should be a lint error rather than a type checker error. But we choose to go ahead and error in the cases that are very likely to be an error: dividing something typed as int or float by something known to be Literal[0].

This isn't definitely an error, because the object typed as int or float could be an instance of a custom subclass which overrides division behavior to handle zero without error. But if this unusual case occurs, the error can be avoided by explicitly typing the dividend as that safe custom subclass; we only emit the error if the LHS type is exactly int or float, not if its a subclass.

a = 1 / 0  # error: "Cannot divide object of type `Literal[1]` by zero"
b = 2 // 0  # error: "Cannot floor divide object of type `Literal[2]` by zero"
c = 3 % 0  # error: "Cannot reduce object of type `Literal[3]` modulo zero"
d = int() / 0  # error: "Cannot divide object of type `int` by zero"
e = 1.0 / 0  # error: "Cannot divide object of type `float` by zero"

reveal_type(a)  # revealed: float
reveal_type(b)  # revealed: int
reveal_type(c)  # revealed: int
# TODO should be int
reveal_type(d)  # revealed: @Todo
# TODO should be float
reveal_type(e)  # revealed: @Todo

class MyInt(int): pass

# No error for a subclass of int
# TODO should be float
reveal_type(MyInt(3) / 0)  # revealed: @Todo