Never is a subtype of all types, this isn’t something I’m suggesting be changed at all.
However, there are plenty of examples where there’s clearly an attempt to use something that statically cannot have a value as a value that causes false negatives because current type checkers do not distinguish between concepts that require a valid value or not. (of which, things with a type of Never can never have a runtime value)
For example:
def example[T: A](foo: T) -> T:
if not isinstance(foo, A):
log.warning(f"Recievied incompatible type {type(foo):!r}")
return foo
else:
foo.bar = 1
return foo
Here, this is assignable purely on type compatibility, but return foo should still be an error of some sort, as a return statement requires a value, and Never means there cannot be a value. fixing an example like this is as simple as changing it to:
def example[T: A](foo: T) -> T:
if not isinstance(foo, A):
typing.assert_never(foo) # will error at runtime
else:
foo.bar = 1
return foo
to error at runtime or
def example[T: A](foo: T) -> T:
if not isinstance(foo, A):
log.warning(f"Recievied incompatible type {type(foo):!r}")
else:
foo.bar = 1
return foo
to retain the same behavior.
This avoids a class of issues where there are false negatives because of runtime errors that mismatch type information.
This might be too restrictive to enable for all value expressions, but it does seem reasonable for this to be an error at function boundaries, either in passing a parameter that cannot exist, or in returning a value that cannot exist rather than explicitly raising.
Just to note current type checkers behaviour on this.
Mypy doesn’t have errors for this by default, but it does have an option to indicate unreachable code (--warn-unreachable) to get some warning for this case. mypy-play
Pyright, for this particular case, currently would show an error in strict mode because isinstance(foo, A) always evaluates to True, pyright-play. Pyright usually just marks unreachable code as greyed out and doesn’t analyze it, but there are no warning or errors. Recently some issue on Pyright on adding unreachable code warning got reopened, so maybe Pyright is going to have a warning/error option for this too.
Pyre seem to have no warnings for this (pyre-check) at first glance. When I added reveal_type(foo) to the unreachable block, Pyre ignored it. So, I guess it’s behavior is a bit similar to Pyright - it skips unreachable code completely without any warning, though unlike Pyright it doesn’t have always-true error for isinstance to cover this case in some way.
Pytype does exactly the same as Pyre.
I agree that it does makes sense to have at least some indication when Never is actually used and passed somewhere, but this issue seems to be part of general issues related to code reachability analysis and covered by unreachable code indication (though to different degree by different type checkers).
Are there any cases when Never can actually occur in reachable code, if user won’t set it manually? And when user would set Never manually? (besides using it or NoReturn as a return type to annotate function that doesn’t return normally)
Through narrowing. If there’s ever a runtime value where a typechecker expects the type of Never, there’s a type issue somewhere because Never, in the type system, can’t have a runtime value.
It’s fine as a return type, because we use this to mark functions that should always raise and should never have a value, but it’s not fine as a value in a return statement because the assignability of Never to all types means that this covers up mishandling runtime type checking, as shown above.
The only time a value with a type of Never can be reachable is when runtime does not match the type information, or in other words, when there is a type error. Use of something with a type of Never as a value is always an indication of a type error by definition, because something with a type Never can’t have a valid runtime value by definition.
The exception here would be typing.assert_never, which is specified for this purpose to handle this mismatch by raising at runtime if it is ever reached, and is designed to be used to assert to the typechecker an actual expectation of unreachability, useful for validating intended exhaustive matching.
It is not always a TypeError since static typing definitions don’t always match runtime behaviour. I assume this is an example of this (although the Never value is not used):
# pyright: strict
from __future__ import annotations
from typing import reveal_type
class A:
def __add__(self, other: A) -> A:
# pyright with strict rejects isinstance here:
if isinstance(other, A):
return A()
else:
return NotImplemented
class B:
def __radd__(self, other: A) -> B:
if isinstance(other, A):
return B()
else:
return NotImplemented
c = A() + B()
reveal_type(c) # B
That’s not a case of using or returning a value with a type of Never (in the else branch, you return a constant NotImplemented), the error you encounter in pyright there is an error that is not part of the type specification, and one I disagree with pyright implementing because it assumes that people will not intentionally handle cases where the wrong type is passed, even though the data model outright requires it.
@oscarbenjamin Thanks for that example, it’s a great showing of why it’s fine for Never to be inferred somewhere and distinguishing between that being the inference, and actually using the value that has an inferred type of Never.
As far as the type system is concerned, when in the else branch there, the type of other should be Never, however, as @Liz pointed out, you’re not using the value there, you’ve eliminated the possibility, and then are doing something still valid. If you instead still tried to return something that relies on the value of other in that branch, that would be the error case.
I’m still trying to formulate the right places this should be an error, but I agree with you that your example is valid, and with Liz that this is a case where pyright has implemented a check that creates noise here. It’s possible pyright could remove these checks from strict if a proper set of rules for use of a value Never being an error were to be specified, as ideally they would cover the cases that this somewhat acts as a heuristic check for currently in a more appropriate manner.
I’m not sure if it is valid. In particular the annotations for A.__add__ are not correct given how it can be validly called (with Any argument). If the method were renamed from __add__ to add then pyright’s behaviour would be correct. I can’t find a source for this now but I think there was something somewhere where some PEP said “let’s make a shortcut and ignore NotImplemented in the type hints…”.
What I do know is that the code I showed is correct and the type annotations have to be written the way that I did or otherwise type checkers will not infer the type of A() + B() correctly (and they still don’t get it right always e.g. pyright gets it wrong if B is a subclass of A). If the annotations do have to be that way then I think __add__ is maybe a special case rather than an example of something more general and the fix is perhaps just that pyright needs to handle that special case better.
With the current specification, this is the right way to indicate to typecheckers the supported types for these methods. I agree it’s a little awkward here.
Even if it weren’t though and we were looking at a function, not a data model method, I think it’s valid to handle cases where the function receives something it isn’t expecting, and to ensure places where people take the time to check this aren’t just ignored by typecheckers. If someone is explicitly checking for this, they are doing runtime validation in a language that doesn’t have this compile time checked, and their return value, even in that case should still be subject to the type system rules.
However, this would require typing.assert_never to be special-cased, and Jelle is against it, instead suggesting that a new primitive is needed.[2]
Including __setitem__ and __setattr__, so x=<Never> or array[index]=<Never> should also error. ↩︎
IMO, having two separate bottom types, one uninhabited and one inhabited, could be confusing and potentially lead to other issues, but it might be worth exploring if other options are not possible. ↩︎
I disagree with a new primitive being needed here, that would defeat the purpose of ensuring there isn’t a reliance on a value that the type system says can’t have a value.
typing.assert_never also doesn’t need special casing here to make a useful rule here.
A combination of the following cases covers the real issues currently hidden by the type system allowing contradictory information about values with a type of Never.
Erroring when Never is assigned to anything other than Never as a value covers this, and leaves it possible to define functions that explicitly handle type system error cases not limited to or requiring the special casing of typing.assert_never
In functions that explictly accept a type of Never, allow use of the values always present on object, as this is the type safe minimum knowledge for when there is a contradiction between annotations and runtime. This allows things like catch-all string formatting, error logging, constructing an exception type containing the type-error in functions designed to handle the error of receiving a value that contradicts the type information at runtime.
Returning a value of Never (ever)
Returning from a function annotated as not returning a value (must raise, not return)
typing.assert_never should be special cased. Type checkers already special case the entire typing module as it is.
I disagree with this. people can use a type: ignore or a cast to object when they are explicitly intending on using a value that the type system says can’t exist, everyone should get errors for using such a value.
Type checkers special case a number of specific symbols in typing, but not necessarily all of them. There are a number of other symbols in the module that should not require special casing (e.g., AnyStr, Sized), and in general I think it’s valuable to keep the number of primitives as low as possible. That way, the behavior of tools like assert_never can flow naturally from the rest of the type system, making it easier to understand and implement in general.
assert_never already violates the rules of the type system currently because it exists to handle the case of when there is a contradiction between type information and runtime. Pretending it doesn’t does not make it easier for people to understand the type system, it makes people misunderstand it, and reach the wrong conclusions when assignment of Never occurs. thinking that it acts as a counter example of something, when in reality, there was a problem with the typechecker in question
Clearly, typing.assert_never breaks the rules, it’s a function that does something with a value that the type system says cannot exist. Never is uninhabited at runtime.
Other languages have better means of handling this. I particularly like zig’s unreachable which is also a special case, and panics if reached in safe compile modes.
I don’t think the question should be if typing.assert_never requires special casing, it absolutely does, but whether or not the special case can exist for all functions that accept a type of Never or if that creates other undesirable behavior.
A new type system construct could help resolve this, and would allow user functions like assert_never to exist, but it would involve changing typing.assert_never and this highlights that it is a special case currently.
@Jelle has brought up a “type error” decorator before IIRC, meant to be used in cases of misuse rather than as deprecated
This still doesn’t solve it unless we ammend the rules (not special case) so that functions that accept Never remain exempt here.
The problem here is Never is only assignable to all types because it is uninhabited. By typecheckers not enforcing the uninhabitability of Never, they violate the reason this works and create false negatives.
We can resolve this while staying within theory with function domain analysis (which is already a requirement for type checkers due to TypeIs and the subtyping rules), but that still requires type checkers error for many things they don’t currently (and absolutely should)
Such a rule would be that it’s illegal to use a value with a type of Never in a function that expects a value, as a domain error. This allows “uncallable functions” such as your overload with a type error on one of the overloads to remain theory sound.
I don’t see a case here for any new guidance or type system features beyond “it’s great if type checkers (at least offer an option to) error on unreachable code.” That’s what Never means: this code can’t be executed. [1]
“Erroring on use of Never” would be a mis-feature that both doesn’t make sense from a type theory perspective, and would cause irritatingly verbose cascading diagnostics, when the better answer (for both UX and consistency) is to just warn once that the entire block is unreachable, and otherwise allow Never to behave as it should (a type that is assignable to anything and has all attributes/methods, also of type Never.)
The __eq__ case is special. Type checkers should probably just silence their unreachable-code warning inside __eq__, since the annotation conventions don’t match the actual possible argument types. ↩︎
I don’t think this is correct. Never cannot have a value. If a statement or expression requires a value, a value with a type of Never cannot exist, and therefore it cannot be compatible because it cannot coexist with the requirement of there being a value. You’re making the mistake of conflating type compatibility of Never with other types, and whether an expression must be an error from type information.
I don’t know if you meant this implicitly but to be clear it isn’t just __eq__ but every binary dunder. I use these a lot and I see annoying unreachable code warnings from pyright all the time in __add__, __radd__, etc. Some classes have unreachable code in practically every method.
They do clearly need to be special-cased but I don’t think silencing the unreachable-code warning is the special casing that is needed. A type checker rather needs to understand that the annotations have a different meaning in this context. That means that this:
def __add__(self, other: A) -> A: ...
should be understood as something like:
@overload
def __add__(self, other: A) -> A: ...
@overload
def __add__(self, other: Any) -> NotImplementedType: ...
def __add__(self, other: A | Any) -> A | NotImplementedType: ...
Then the type checker should silence its complaint about the overlapping overload with NotImplementedType as the return type.