# Interactions with Never leading to undesirable assignability

**URL:** <https://discuss.python.org/t/interactions-with-never-leading-to-undesirable-assignability/99445>\
**Category:** Typing\
**Created:** [July 20, 2025, 6:00am UTC](https://discuss.python.org/t/interactions-with-never-leading-to-undesirable-assignability/99445 "2025-07-20T06:00:29Z")\
**Posts on this page:** 1\
**Showing post:** 36

<div class="post-metadata">

**Author:** ![ruro](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/ruro/32/7340_2.png) [@ruro](https://discuss.python.org/u/ruro)\
**Post date:** [July 25, 2025, 7:39pm UTC](https://discuss.python.org/t/interactions-with-never-leading-to-undesirable-assignability/99445/36 "2025-07-25T19:39:18Z")

</div>

> [@Jelle](#):
>
> But a TypedDict must be an instance of dict (not a subclass) with those exact keys, and there cannot be a dict with a key `b` and no value. Therefore, `TD1` with `b` materialized to `Never` and `TD2` with `d` materialized to `Never` are both empty types, i.e., `Never`.

It seems to me that you are making a hidden assumption here. Let’s completely ignore gradual typing and materialization for a second. Consider the following completely statically typed program:

```python
from typing import TypedDict, Never

class ADictWithNever(TypedDict):
    never: Never

def func(d: ADictWithNever) -> None:
    assignable_to_never: Never = d

```

According to your logic, this should pass type checking. Both mypy and pyright currently don’t accept this. In fact, I think that they **shouldn’t be allowed** to accept this (more on that later).

Your argument seems to be that `Never` and `ADictWithNever` should be structurally equivalent types, because we “know” that they both denote an empty set of runtime values. I don’t think that you can actually prove that `ADictWithNever` denotes an empty set **only using nominal/structural information** that is available to the type system.

According to the definition of `TypedDict`, we know that `ADictWithNever` is a structural type that satisfies the following structural requirements:

1. It is a dictionary object (and not a subtype of `dict` or `Mapping`, but `dict` specifically).  
Or in other words, `type(d) == dict` is guaranteed to be `True`.

2. It is required to have a key named `never`.  
Or in other words, `"never" in d` is guaranteed to be `True`.

3. The value of that key is of type `Never`.  
Or in other words, `d["never"]` is guaranteed to be assignable to `Never`.

4. (and a bunch of other similar structural requirements, the exact list of which is seemingly never actually explicitly specified as if it is obvious, but seems to boil down to “`d` quacks like a `dict` that has a `"never"` key with a value of type `Never`”)

Now, as a human, you know how `dict` is actually implemented and so you can infer that it’s **impossible** to construct a `dict` that ` __contains__ ("never")` and also “never returns” from ` __getitem__ ("never")`. And so you make a fairly reasonable inference that `ADictWithNever` must correspond to an empty set (of possible runtime values).

Type checkers on the other hand don’t have enough information about the runtime implementation details of the `dict` type to make such an inference. Type checkers only have access to nominal and structural type information, which is ratified in the various typing PEPs and encoded in typeshed hints (or sometimes hardcoded into the typecheckers themselves for information that can’t be directly expressed in the language).

From the perspective of the type checker, there might as well be some valid function

```python
def create_adictwithnever_pretty_please() -> ADictWithNever: ...

```

that actually constructs a concrete object `d`, such that `type(d) == dict` and `"never" in d` is `True` and `d["never"]` raises a `CantTouchThat` exception or loops forever without returning or whatever. So from a type-theoretical perspective, `ADictWithNever` denotes some set of values, but the type system doesn’t have enough information about this set of values to prove that it is empty. And so `ADictWithNever` is not assignable to `Never` (which **is** provably empty by definition and thus distinct from `ADictWithNever`).

* * *

As an aside, I am not sure if this is actually specified anywhere, but I think that type checkers shouldn’t even be allowed to make inferences that can’t be completely derived from information that is “known” or expressed in the type system. Here’s a silly example:

```python
def foo(v: int) -> None:
    if type(v) != int: return
    if v < 0: return
    if v > 0: return
    if v == 0: return
    # Clearly, the set of possible values of v is empty at this point, right?

    # Should type checkers be allowed to infer this fact?
    i_dont_think_so: Never = v

```

Unless and until a new typing PEP is accepted which formally defines the structural properties of `int`s, the above code ought to be rejected by type checkers, imho. The same applies to “containers that provably have at least one instance of `Never`”.

---

_[View the full topic](https://discuss.python.org/t/interactions-with-never-leading-to-undesirable-assignability/99445)._