Edge case: mypy ignores Never being passed as an argument to another function.

[randolf-scholz]

Bug Report

This is kind of a version 2.0 for #15818, as I found an edge-case where mypy silently passes an instance of Never.

from typing_extensions import Never

def never_returns() -> Never:
    raise NotImplementedError

def g(x: str) -> str:
    return x

def h() -> str:
    return g(never_returns())  # no warning raised here

g(never_returns())  # no warning raised here
# only if there was code after it we would get [unreachable]-error.

(mypy-play with --strict and --warn-unreachable)

Expected Behavior

The above code should raise on lines containing g(never_returns()), as instances of Never cannot exist, and hence cannot be passed as arguments to other functions. Therefore, the only safe behavior is that functions that return Never can only appear "on their own", their output cannot be assigned to variables (the same code as above with x=never_returns() in the last line gives the unhelpful message "Need type annotation for "x"") or be part of an expression:

never_returns()   # OK
(never_returns() for x in range(3))  # maybe OK?
x = never_returns() # not OK
g(never_returns()) # not OK

The --warn-unreachable flag is useless when the offending code appears in the last line of a script / function definition.

[erictraut]

Mypy is correct in not generating an error here. The type Never is a subtype of all other types, so it's type compatible with str. Pyright also does not generate an error here for the same reason.

Practically speaking, if the function never_returns never returns control back to the caller, then it doesn't violate any type rules for the caller.

If this were a common source of bugs, I suppose that a type checker could emit a warning in this case even though it doesn't violate any type rules. However, I don't think this is a common source of bugs. Your sample looks pretty contrived to me.

[randolf-scholz]

@erictraut I completely agree that Never is compatible with str, but the issue is that for it to be able to be passed, an instance of Never has had to exist in the first place. But instances of Never are not allowed:

Python docs:

The bottom type, a type that has no members.

In other words, it is an axiom that no instances of type Never can exist. The cited Wikipedia article states:

If a type system is sound, the bottom type is uninhabited and a term of bottom type represents a logical contradiction. In such systems, typically no distinction is drawn between the bottom type and the empty type, and the terms may be used interchangeably.

If the bottom type is inhabited, its terms[s] typically correspond to error conditions such as undefined behavior, infinite recursion, or unrecoverable errors.

If a type can have no members, a type-checker should probably raise an error if such a member was provably brought into existence. A bare never_returns() could be considered OK since are no "witnesses" that an instance of Never ever existed. However, if we use the output of never_returns() as input for something else, that something else becomes a witness of an instance of Never.

[randolf-scholz]

Practically speaking, if the function never_returns never returns control back to the caller, then it doesn't violate any type rules for the caller.

But even under this view, shouldn't it at least produce an unreachable-error? Since the calling of the outer function is never reached?

[erictraut]

I don't think it's a bug, so I would categorize it as an enhancement request. The maintainers of mypy can decide what they would like to do here. As for pyright, I don't plan to emit any errors here because it's not a type violation and it's not a common bug pattern.

[randolf-scholz]

So the second half sentence in "The bottom type, a type that has no members." is basically meaningless to type-checkers? Or do they intentionally ignore it for some pragmatic reason?

[JelleZijlstra]

The fact that a type has no members doesn't imply that it is an error to use it.

[randolf-scholz]

The fact that a type has no members doesn't imply that it is an error to use it.

It's a logical contradiction to simultaneously assume (1) instances of Never do not exist and (2) an instance of Never was passed as an argument to another function.

[A5rocks]

To chime in with my opinion:

Never doesn't exist as far as type checkers know. However, being able to pass it places has (very!) practical benefits such as:

• making sure exhaustive checks are exhaustive
• deprecations that aren't in the type signature but you still warn about
• more helpful handling of type-level impossible values

We're better off for all of those.

As such, practicality over purity and this is allowed. At least that's how it seems to me. If this is actually causing you errors, maybe things can be rethought.

(Additionally, I don't see why you seem to expect type checkers to consider whether a function can be called when saying if it's type safe...? Like I don't think this violates purity either, I am providing an argument that doesn't rely on purity)

[randolf-scholz]

@A5rocks Can you give an example?

making sure exhaustive checks are exhaustive

Not sure how the proposal here would stop you from doing exhaustive checks.

deprecations that aren't in the type signature but you still warn about

We'll have https://peps.python.org/pep-0702/ for that.

more helpful handling of type-level impossible values

When and how is this useful?

[randolf-scholz]

Never is the bottom type.

1. The bottom type is a subtype of every type.
2. The bottom type is uninhabited.

Being strict about ② is really useful, for example, consider a function get_last that returns the last element of a list, and None if the list is empty. I'd argue that the correct way to type hint this function is with:

@overload
def get_last(x: list[Never]) -> None: ...
@overload
def get_last(x: list[T]) -> T: ...

Given input x of type X, the return type can be deducted as follows:

1. Determine if X <: list, if not: error!
2. Else, assume X = list[Y].

• If Y = <nothing>, match with first signature, return None.
• If Y = Never, error! This violates the axiom that Never is uninhabited
• Else, match with second signature, return Y

That is, I argue that Never, when used as an annotation in a function signature argument, should only ever match with <nothing>. So, list[Never] should match only with the empty list, and not some nonsense like [raises_unconditionally()].

I can't see any case where something like x = [raises_unconditionally()] would make any sense¹; possibly it's just my ignorance, but in any case it would violate axiom ②. One can decide to drop this axiom, at the cost of the type-checker being able to make less useful deductions.

¹: except possibly for unit tests that check that the error raising happens in the first place, but even then this is likely covered by allowing bare raises_unconditionally(). A better solution for this is the proposed typing_error or generic Never: python/typing#1043 (comment)

[A5rocks]

Here's an example of exhaustiveness checking, with a deprecation:

import enum
import typing

class A(enum.Enum):
  x = "X"
  y = "Y"

def f(x: A) -> str:
  if not isinstance(x, A):
    # this function used to take "X" or "Y", maybe?
    print(f"Make sure you pass `A.x` or `A.y`; not {x!r}")
    x = A(x)  # we're using a Never here

  if x is A.x:
    return "A"
  elif x is A.y:
    return "B"
  else:
    typing.assert_never(x)  # we're using another Never here

[randolf-scholz]

typing.assert_never would unsurprisingly need to be special-cased, this is a bit of a corner case.

For the first part, f should be annotated as f(x: A | Any) or have overloads if it is supposed to accept things different from A, for instance:

@overload
def f(x: A) -> str: ...
@overload
@deprecated("Only A will be allowed in the future")
def f(x: Other) -> str: ...

[JelleZijlstra]

assert_never() isn't meant to be special-cased. Once again, what you're looking for is not Never but some new primitive. As others have explained, there's no bug here.

[randolf-scholz]

Then the docs need to be changed, as

The bottom type, a type that has no members.

Clearly is violated by the major type-checkers.

[JelleZijlstra]

We can discuss a documentation change over on the CPython repo, but I wrote that documentation and I don't think "has no members" implies that type checkers should error on usage of Never.

[randolf-scholz]

@JelleZijlstra The following doesn't emit any errors, even with --strict.

from typing import Never

def f() -> Never:
    while True:
        pass
    
x: Never = f()

So the type checker has allowed me to create a member of Never.