Ah, I see your point. Yes, it might be useful to have some diagnostics even in the case where “formal” type theory has already decided that the types are contradictory / code is unreachable. Although, I am struggling to come up with a framework that would automatically detect the “pathological” cases (like the return TypeError(...) example you mentioned) while also not producing false positives.
My own pedantic opinion is that such diagnostics depend on semantics (that are not observable from within the type system) and thus belong in linters, not type checkers. But I can understand and appreciate that there may be some good reasons to include such errors in type checkers, even if they are technically not type errors.
As long as we both agree that bottom / uninhabitable types in general don’t have to be errors and that the current definition of Never is perfectly sound. That sys.exit() -> Never is a valid annotation and that there are cases where unreachable code shouldn’t be considered an error.
P.S. I believe, that we’ve gotten somewhat off-topic. My original point was that Uninhabited is a horrible name for the Wrong / Illegal / Invalid / Forbidden type proposed in this thread, because it makes that same incorrect assumption about how bottom types are supposed to work.
Part of the point being discussed is related to the fact that this thread was linked as a possible solution for another problem, so clearing up that the bottom type isn’t that magical is sort of being discussed as part of two threads at once, and there’s no good way to discuss that on discourse without either getting repetitive or assuming people are seeing that it was linked and seeing why.
Overall, anything that conveys “Error” or “user defined static error message”, while still having the type system semantics as equivalent to Never will be useful as a special form to help pass more useful diagnostic messages for specific cases.
Any reasonable naming that doesnt try and subsume a type system concept should be fine for that.
These are exactly the kind of examples I discussed in my first comment. Did you bother to read it before commenting? My point is exactly that these are the cases that should have been handled with a typing decorator, rather than introducing NoReturn as a type. Instead of
If you like. The issue is that Never was overloaded with two meanings that should have been kept separate, imo. Instead, we now have to deal with type checkers allowing uninhabited types to be inhabited and other oxymoronic statements. The way this is handled at the moment also causes actual false negative unreachable detection: Code sample in pyright playground, mypy-playground
from typing import Never
def foo() -> Never:
while True:
pass
def bar() -> tuple[int, ...]:
return (foo(),) # undetected unreachable code
x = bar()
x += (1,2,3)
from typing import Never
def very_sound_function() -> float:
y: list[Never] = []
return next(iter(y)).startswith("xyz") # type checker approved!
# ^^^^^^^^^^^^^ this may have been a good place to error
# if we really believed Never was uninhabited.
def make_never() -> Never:
while True:
pass
x: Never = make_never() # yep, totally uninhabited.
All of those statements are reached, even if the statement itself is never finished without raising.
in the first one, next throws a stopiteration exception, so the .startswith is never reached, nor is the return. The line itself is reached, so I’m not sure what you want a typechecker to error about there.
Same with the last assignment with make_never. If that wasn’t allowed, assert_never can’t work for exhaustive matching, and sys.exit() would be determined as unreachable.
Yes. I have read your comment. Have you read mine?
I didn’t directly address your suggestion of using a decorator for no_return, because your suggestion is based on a faulty assumption that bottom types are currently broken.
Both the examples you gave (def bar(): return (foo(),) and very_sound_function) and the example that I gave earlier (run_task_and_print_result) are perfectly valid, type safe code. These examples do NOT demonstrate “uninhabited types being inhabited”.
“Uninhabited” doesn’t mean “no variable has this type”, like you seem to think. “Uninhabited” means “there is no value of this type”:
A value is said to inhabit a type if it is a member of the set of values represented by that type. For example, the value 42 inhabits the type int, and the value "hello" inhabits the type str.
The expressions foo() and next(iter(y)) (and result = task() when T is Never in my example) have the type Never and indeed they never take on any concrete value. Therefore, they are uninhabited.
This is valid, type safe code. The type system detects type safety violations. Unreachable code is not a type safety violation.
The behavior that you are observing (that you can do basically arbitrary stuff to expressions and variables of type Never) is a feature. That is how bottom types are supposed to work. That is how they work in other languages. Because that is how type theory defines them to work.
Never was never (ha) overloaded with two meanings. Instead, users like you have assumed that Never has a second meaning beyond “this is a bottom / uninhabited type”.
This thread proposes adding a new Wrong type that actually would have the second meaning (the meaning being “having any expressions of this type in your code is an error”). But that would be a custom extension over the standard bottom type semantics.
Btw, @JoniKauf this whole discussion about unreachable code made me notice that even for Wrong, we still might be lumping together multiple expectations.
Perhaps, we could further distinguish Never, NeverUse and NeverAppears (names intentionally left un-bikeshedded).
Specifically,
# Never == NoReturn is just a bottom type
def normal_uninhabited_value() -> Never: ...
# this is okay
normal_uninhabited_value()
# this is also okay
variable = normal_uninhabited_value()
variable.do_arbitrary_stuff_with_results()
# NeverUse is also a bottom type, but it **must** be discarded
def value_should_not_be_used() -> NeverUse: ...
# this is okay (since the value is immediately discarded)
value_should_not_be_used()
# but THIS is not okay
variable = value_should_not_be_used() # error
# and neither is THIS
value_should_not_be_used().do_arbitrary_stuff_with_results() # error
# NeverAppears is also a bottom type and it **should not** appear as the type of any expression
def value_should_never_appear_in_an_expression() -> NeverAppears: ...
# this is okay (Callable[[], NeverAppears] is not an instance of NeverAppears)
# (not calling the function here, just reassigning it)
foo = value_should_never_appear_in_an_expression
# but any of the following are errors since there is an expression of type NeverAppears
value_should_never_appear_in_an_expression() # error
variable = value_should_never_appear_in_an_expression() # error
value_should_never_appear_in_an_expression().do_arbitrary_stuff_with_results() # error
Of course, a proper PEP might also want to consider if NeverUse and/or NeverAppears should be decorators instead (although I personally don’t see the appeal).
My understanding is that the current proposed semantics of Wrong / Invalid / Forbidden are closer to NeverAppears, but it is evident that some people that abuse Never expect the second behavior (i.e. you are allowed to call a function that returns such a type, but attempting to use the resulting value (or even having any code after the call) is an error).
I like the idea of 2 different kinds of a new bottom type to indicate different errors if there is a purpose to them. Do you have any concrete examples where NeverUse could be useful?
Take a look at the recent discussion with Randolf here.
I think that the NeverUse “semantics” are more or less what they were expecting Never / NoReturn to mean. That is - a function that is okay to call, but that is guaranteed to never return and therefore the return value should not be used, and no code should follow after the call.
Basically, NeverUse would be an explicit request to check for dead / unreachable code at the call site. Concretely, I would expect this type to be useful, when a user might erroneously believe that a function returns some value (and write some code trying to use that value), while in reality the function never returns.
Maybe something like
def user_code() -> None:
# user expects process_requests to return the results
results = somelib.process_requests()
for result in results:
blah_blah_blah(result)
# but in somelib, process_requests
def process_requests(
# actually expects an optional callback
result_callback: None | Callable[[Result], None] = None,
# and never returns
) -> Never:
with Connection() as conn:
while True:
result = conn.get_next_result()
try:
if result_callback is not None:
result_callback(result)
except Exception as e:
handle_exception(e)
This would currently pass type checking, but replacing Never with NeverUse would explicitly signal to the user that attempting to use the uninhabited return type of process_requests is probably an error.
Honestly, I am speculating a bit here. It’s clear that some users want type checkers to detect dead code. And while I personally think that this is the wrong place for such diagnostics, it might be better to provide them with a special type / decorator for that, just so that we can point to this type / decorator when people complain that Never doesn’t work like they expected.
It would probably fine to annotate sys.exit with NeverUse.
For examples, where Never should not be replaced with NeverUse, see Carls sys.version_info >= (3, 14) example or my run_task_and_print_result example.
Basically, any case where:
the bottom type occurs implicitly or “naturally” as a consequence of narrowing, type guards or other typing interactions
or the function is intended to be used in a generic context (and T is only Never sometimes)
or when you need to use the covariance properties of return value types in order to express that your function is a subtype of functions with any return types
or when you want to restrict the return type of a method during inheritance
In most “trivial” cases, such as sys.exit, you can probably replace -> Never with -> NeverUse. But not all cases are trivial, and determining which cases can / should be replaced with -> NeverUse requires understanding the semantics of the code (and so can’t be done automatically).
I’m not convinced by those 2 examples (the sys.version_info one doesn’t seem to have any place where a user would ever provide a NeverUse annotation, while the run_task_and_print_result example doesn’t seem to have an obvious place where errors would be reported even if NeverUse was used).
However:
Thank you, I can see the case for Never over NeverUse in #2, #3, and #4 above. (I’m not quite convinced by #1, which is just a generalisation of the sys.version_info example.)
Based on how similar errors are currently rendered by pyright, I would imagine that the error would be reported at the call site where T is attempted to be substituted for NeverUse:
run_task_and_print_result(do_stuff_forever_task)
and the error message might look something like
error: Argument of type "() -> NeverUse" cannot be assigned to parameter "task" of type "() -> T@run_task_and_print_result" in function "run_task_and_print_result"
Type "() -> NeverUse" is not assignable to type "() -> T@run_task_and_print_result"
Function body contains usage of values of type "T" (neverUseIsUsed)
Of course, you might argue that this error message can be hard to interpret, because it doesn’t indicate, which line in run_task_and_print_result “uses” T, but in my experience type checker errors can be a bit arcane even when you aren’t trying to make your type checker do the job of a linter.
So I am not sure, if this is an issue with this particular problem / example.
Oh, okay - looking inside the function body for potential uses when triggered from a calling context is a far more intrusive kind of analysis and reporting than I was expecting NeverUse to offer in reality.
I was looking at that example without any of the function bodies, because I’d expect error reporting to be consistent regardless of whether a function was used from a definition in the same file, defined from another .py, or defined from another .pyi.
NeverUse reads like “it can be assigned but never used later”, which is not the semantic wished here I guess. NeverAssign conveys more precisely that the return value should never be assigned.
I am open to alternative names, however NeverAssign doesn’t work, because it misses stuff like never_use().do_stuff_with_return_value() and other usage patterns that don’t assign to an intermediate variable.
I chose the name NeverUse, assuming that assignment itself is also just a kind of usage. Basically, the only thing you are supposed to do with a NeverUse is immediately discard it.
If we didn’t already have NoReturn, I would probably suggest using that instead of NeverUse. Then we could have the trio of Never (pure uninhabited type, no extra constraints), NoReturn (also uninhabited, but checks that the return value isn’t used anywhere) and Invalid (also uninhabited, but represents the fact that this function shouldn’t be called at all). But I am not sure if the churn of changing the behaviour of NoReturn is worth it.
I’d say the confusion most people seem to be running into between Never & NoReturn means that the churn wouldn’t be that bad. I’d support addingInvalid and changing the meaning of NoReturn
The use of Never / NoReturn requires code flow analysis. The code must be analyzed to prove if the types are actually uninhabited. “Naive” type checking approaches that only look at the type hints without unreachable code analysis will always be deficient when dealing with these types.
NoReturn as it name implies is a function return type which marks a function as not “returning normally”. The only way for the function to exit should be to raise an exception explicitly or implicitly, including KeyboardInterrupt and SystemExit, and other interpreter-generated exceptions such as MemoryError. Similarly goes for Never.
return next(iter(y)).startswith("xyz")
The very_sound_function function raises an exception and never returns normally. It would be better if type checkers can specifically indicate that a StopIteration is being raised by the next here, and that dot lookup of the name startswith is unreachable.
Chainging Never in the y: list[Never] = []to str and it also type checks fine[1]
x: Never = make_never()
Since the function call make_never() never returns normally (the only way for it to exit is for the interpreter to raise an exception), the assignment operation to the name x is unreachable. Thus, x never gets actually inhabited.
That said, I’m not opposed to the introduction of more specific special forms that convey the practical meanings better than the abstract notion of a “bottom type”. But the existing uses of NoReturn / Never should not be made invalid by the change.
For the totally different rabbit-hole of why a function with return type float should be compatible with a bool . ↩︎
because it can be applied also for 
.