# Better specification for when the presence of typing.Never should be considered a type system error

**URL:** <https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757>\
**Category:** Typing\
**Created:** [April 26, 2025, 6:41pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757 "2025-04-26T18:41:01Z")\
**Posts on this page:** 20\
**Page:** 2

<div class="post-metadata">

**Author:** ![mikeshardmind](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/mikeshardmind/32/14381_2.png) [@mikeshardmind](https://discuss.python.org/u/mikeshardmind)\
**Post date:** [April 28, 2025, 11:30pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/21 "2025-04-28T23:30:14Z")

</div>

> [@mikeshardmind](#):
>
> ```python
> def example[T: A](foo: T) -> T:
> if not isinstance(foo, A):
> log.warning(f"Recievied incompatible type {type(foo):!r}")
> return foo # violates the return type
> else:
> foo.bar = 1
> return foo
> 
> ```

I still maintain that this example from the very first post demonstrates the problem without relying on the underspecification of dunder methods.

This is **not** unreachable code at runtime because python as a language does not enforce this, and the return value being Never here being considered compatible without enforcing uninhabitability causes this to be a faultily implemented runtime check that is a false negative which would have been properly caught by the type system if type checkers insisted on values with an inferred type of Never not being used as a value.

> [@mikeshardmind](#):
>
> 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.

---

<div class="post-metadata">

**Author:** ![carljm](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/carljm/32/959_2.png) [@carljm](https://discuss.python.org/u/carljm)\
**Post date:** [April 29, 2025, 2:38pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/22 "2025-04-29T14:38:40Z")

</div>

Yes, you’re right. It also includes other dunders, and there would be more sophisticated options for special-casing them that would give even better results.

I mentioned “silencing unreachable code” as the simplest possible option; next would be “treat the argument as `object` inside the function, even though it’s annotated with a more precise type”, and the third level would be to also model the possibility of a `NotImplemented` return in the external signature, as your overload does.

(BTW, I don’t think there’s a case for the use of `Any` or gradual typing here; I would modify your example so the second overload and the implementation signature both simply have `other: object`.)

---

<div class="post-metadata">

**Author:** ![carljm](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/carljm/32/959_2.png) [@carljm](https://discuss.python.org/u/carljm)\
**Post date:** [April 29, 2025, 2:48pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/23 "2025-04-29T14:48:17Z")

</div>

> [@mikeshardmind](#):
>
> If a statement or expression requires a value

_Every_ statement or expression “requires a value”; it cannot possibly execute without one. That’s why a type of `Never` always means unreachable code. Following this train would result in erroring on every line of code inside any unreachable block, or else inventing ever more arcane heuristics about where to error and where not to error.

There is nothing wrong, from a type perspective, with the statement `return foo`, where `foo` has type `Never` (that is, we are in unreachable code.) For there to be a type problem, there would have to be the possibility that `return foo` returns some object that does not inhabit the annotated return type of the function. If `foo` has type `Never` at that point, there is no possibility of that occurring, because the `return` statement cannot execute without a value.

Erroring on `return foo` (and every other line in the block mentioning `foo`) is just noise. The correct diagnostic, if any, is at the point where `foo` takes on the type `Never` (that is, where we entered unreachable code.)

> [@mikeshardmind](#):
>
> This is **not** unreachable code at runtime because python as a language does not enforce this

From the point of view of a type checker, it is unreachable code. `foo` must be a subtype of `A`, therefore the `isinstance` check will always return `True`, therefore the branch is unreachable.

If we start emitting diagnostics based on “maybe the type annotations are just wrong”, then we are in nonsense territory – the only thing a type-checker could ever do is throw up its hands and emit an “I have no idea” diagnostic on every line of code.

If the annotations are indeed wrong (and this is not caught at a call-site), a single “unreachable code” diagnostic is sufficient to highlight and diagnose that problem.

---

<div class="post-metadata">

**Author:** ![mikeshardmind](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/mikeshardmind/32/14381_2.png) [@mikeshardmind](https://discuss.python.org/u/mikeshardmind)\
**Post date:** [April 29, 2025, 3:02pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/24 "2025-04-29T15:02:30Z")

</div>

> [@carljm](#):
>
> > [@mikeshardmind](#):
> >
> > This is **not** unreachable code at runtime because python as a language does not enforce this
> 
> From the point of view of a type checker, it is unreachable code. `foo` must be a subtype of `A`, therefore the `isinstance` check will always return `True`, therefore the branch is unreachable.
> 
> If we start emitting diagnostics based on “maybe the type annotations are just wrong”, then we are in nonsense territory – the only thing a type-checker could ever do is throw up its hands and emit an “I have no idea” diagnostic on every line of code.

I don’t agree here. There’s two possible interpretations here.

1. It’s an error to even have unreachable code. This precludes libraries from having type annotations, but still having sensible runtime checks for their users that may not have typed code bases (especially with libraries that interact with system calls, cffi, etc and preventing catastrophic issues…) while still preventing incorrect use in the library statically. This attitude could only make sense in the case of application code given the lack of compile time checks.
2. It’s an error to rely on values of Never. This would only error on the `return foo` line in that example, which catches a place where a place the type checker _knows_ there must be a contradiction in type information from escaping that scope. It would still be valid to raise an error here instead (and likely the “correct” behavior for code of this pattern).

There are sensible ways to restrict what is allowed in scopes like this that would not cause every single line to be an error.

And as an amusing aside, the choice to error for unreachability would still require that typing.assert\_never must be special cased, to exclude it from such a diagnostic, given its purpose in statically asserting such unreachability/exhaustive matching.

---

<div class="post-metadata">

**Author:** ![Liz](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/liz/32/15021_2.png) [@Liz](https://discuss.python.org/u/Liz)\
**Post date:** [April 29, 2025, 3:21pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/25 "2025-04-29T15:21:25Z")

</div>

> [@carljm](#):
>
> If we start emitting diagnostics based on “maybe the type annotations are just wrong”, then we are in nonsense territory – the only thing a type-checker could ever do is throw up its hands and emit an “I have no idea” diagnostic on every line of code.

You’re wildly strawmanning the proposal here. This isn’t “maybe the annotations are wrong, but maybe all annotations are wrong” this is “the annotation for this specific variable _must_ be wrong if this condition is reached, error for further use of this specific variable for which we know there must be something wrong while that condition remains true to prevent one error in this location from escaping to other locations”

---

<div class="post-metadata">

**Author:** ![jorenham](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/jorenham/32/27806_2.png) [@jorenham](https://discuss.python.org/u/jorenham)\
**Post date:** [April 29, 2025, 11:24pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/26 "2025-04-29T23:24:57Z")

</div>

> [@Liz](#):
>
> it makes people misunderstand it, and[reach the wrong conclusions when assignment of Never occurs.](https://discuss.python.org/t/indexing-typeddict-with-a-non-literal-variable/88929/8) thinking that it acts as a counter example of something

I agree that `assert_never` is confusing. But in my post that you’re referring to, I wasn’t using `Never` as a counter example or something. I was trying to show that the referenced example would not be affected by the proposed change we were discussing. It wouldn’t have mattered if it instead returned `Any` or `Unknown`.

---

<div class="post-metadata">

**Author:** ![Liz](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/liz/32/15021_2.png) [@Liz](https://discuss.python.org/u/Liz)\
**Post date:** [April 30, 2025, 4:43pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/27 "2025-04-30T16:43:13Z")

</div>

> [@jorenham](#):
>
> But in my post that you’re referring to, I wasn’t using `Never` as a counter example or something. I was trying to show that the referenced example would not be affected by the proposed change we were discussing. It wouldn’t have mattered if it instead returned `Any` or `Unknown`.

This is incorrect. It was covered up by pyright incorrectly narrowing incorrectly, and that resulted in a false negative that was only hidden because typecheckers do not insist on Never not having values. The bug in question is something Eric has fixed, and your example fails to actually function as an example of what you thought it did.

---

<div class="post-metadata">

**Author:** ![jorenham](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/jorenham/32/27806_2.png) [@jorenham](https://discuss.python.org/u/jorenham)\
**Post date:** [April 30, 2025, 7:22pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/28 "2025-04-30T19:22:11Z")

</div>

> [@Liz](#):
>
> The bug in question is something Eric has fixed, and your example fails to actually function as an example of what you thought it did.

What exactly was I _thinking_ that it did, then?

---

<div class="post-metadata">

**Author:** ![Liz](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/liz/32/15021_2.png) [@Liz](https://discuss.python.org/u/Liz)\
**Post date:** [April 30, 2025, 7:39pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/29 "2025-04-30T19:39:43Z")

</div>

> [@jorenham](#):
>
> What exactly was I _thinking_ that it did, then?

Assuming you weren’t lying, you were thinking what you said about it.

> [@jorenham](#):
>
> I was trying to show that the referenced example would not be affected by the proposed change we were discussing.

It was affected, and is properly detected as an error now that pyright has fixed it’s logic on narrowing in open typed dicts.

Allowing things with a type of Never to be used as a value not only hides misuse by developers, but also masks other narrowing bugs in typecheckers.

---

<div class="post-metadata">

**Author:** ![mikeshardmind](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/mikeshardmind/32/14381_2.png) [@mikeshardmind](https://discuss.python.org/u/mikeshardmind)\
**Post date:** [April 30, 2025, 8:06pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/30 "2025-04-30T20:06:46Z")

</div>

can we please dial the tone down a bit here?

* * *

Here’s my analysis.

1. typed python code is not a closed system and may be called by unchecked code
2. The existence of Never does **not** indicate _only_ unreachability, it also may indicate that at some point, a contradiction has been introduced, either by unchecked code calling, or by other faulty logic, such as an incorrectly implemented TypeIs function, or a bug in a typechecker.
3. In the case of Never, we should assume that _if_ it is reached, there is faulty information somewhere, and that using it as anything more than `object` is an error. Using it as `object` may still be valid, because typed code knows it may be called by untyped consumers, treating it as entirely unchecked is incorrect for the same reason, as would treating it as Any. This is a consequence of typed code not being in a closed system, we can detect _specific_ cases that we know must be _either unreachable or in error_, and then still allow the use if it is reachable as only that which is present on all objects.

If we want to keep existing typechecker behavior of treating Never solely as unreachable, rather than “unreachable, or external error which may be partially recoverable” I’m going to suggest that user-expressible intersections may be a mistake to allow because of other issues of this sort which arise, but will continue with the draft in knowledge of this defect, and outline where it becomes a problem in the draft for others to evaluate the merits and tradeoffs of.

---

<div class="post-metadata">

**Author:** ![jorenham](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/jorenham/32/27806_2.png) [@jorenham](https://discuss.python.org/u/jorenham)\
**Post date:** [April 30, 2025, 8:49pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/31 "2025-04-30T20:49:41Z")

</div>

> [@Liz](#):
>
> Assuming you weren’t lying, you were thinking what you said about it.
> 
> > [@jorenham](#):
> >
> > I was trying to show that the referenced example would not be affected by the proposed change we were discussing.
> 
> It was affected, and is properly detected as an error now that pyright has fixed it’s logic on narrowing in open typed dicts.

We can agree on that. What I’m disputing is your claim that I misunderstand `Never`. Because as I’ve said before, _if_ it would have been the case that instead of `Never` it returned `Any`, then my point would still stand. Put differently, my interpretation of `Never` was irrelevant. That’s why I don’t agree that my post shows that I misunderstand `Never`. Besides, it would be pretty strange if it did, because I’m pretty sure that I understand `Never` :).

---

<div class="post-metadata">

**Author:** ![Liz](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/liz/32/15021_2.png) [@Liz](https://discuss.python.org/u/Liz)\
**Post date:** [April 30, 2025, 8:58pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/32 "2025-04-30T20:58:59Z")

</div>

Your example doesn’t make sense if you understood `Never`, because your example never should have involved `Never`, but rather `object`. The only reason `Never` showed up was because of a typechecker bug that should have been obvious if you understood that `Never` is uninhabitable. Perhaps you misunderstood something else in play, and not `Never`, but I’ve been taking your words at face value, and that’s what your words have indicated to me.

However, we’re now very off-topic here unless you want to use this to support that `Never` can be incorrectly inferred, and should only ever occur in the case of an error or unreachability, and therefore simply being silent about it causes false negatives that are prone to misunderstanding.

---

<div class="post-metadata">

**Author:** ![jorenham](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/jorenham/32/27806_2.png) [@jorenham](https://discuss.python.org/u/jorenham)\
**Post date:** [April 30, 2025, 11:36pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/33 "2025-04-30T23:36:26Z")

</div>

> [@Liz](#):
>
> Your example doesn’t make sense if you understood `Never`, because your example never should have involved `Never`, but rather `object`. The only reason `Never` showed up was because of a typechecker bug that should have been obvious if you understood that `Never` is uninhabitable. Perhaps you misunderstood something else in play, and not `Never`, but I’ve been taking your words at face value, and that’s what your words have indicated to me.

Nope, I understood everything just fine. Thanks for your concern.

Next time, I would appreciate it if would not use my (valid) example, or anyone else’s for that matter, as a means to show that a concept is not well understood. This time, it wasn’t the case, but nonetheless provoking, insulting, and a waste of my time.  
But even if it would actually have been the case, then it would be rather humiliating for that person: No one wants to be used an example of not understanding something. So please be a bit more careful about this in the future.

---

<div class="post-metadata">

**Author:** ![Liz](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/liz/32/15021_2.png) [@Liz](https://discuss.python.org/u/Liz)\
**Post date:** [April 30, 2025, 11:51pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/34 "2025-04-30T23:51:52Z")

</div>

> [@jorenham](#):
>
> Nope, I understood everything just fine. Thanks for your concern.

Clearly not, as your example isn’t valid and does not serve to demonstrate what you claim it does. I don’t say this to cause offense, but because this is a matter of logical application and getting it wrong actually matters in determining the correct behavior for specification purposes. Please do not try to read correcting something as intending to humilate, that’s never my intent.

---

<div class="post-metadata">

**Author:** ![jorenham](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/jorenham/32/27806_2.png) [@jorenham](https://discuss.python.org/u/jorenham)\
**Post date:** [May 1, 2025, 12:21am UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/35 "2025-05-01T00:21:13Z")

</div>

> [@Liz](#):
>
> Please do not try to read correcting something as intending to humilate, that’s never my intent.

I assumed that it wasn’t intentional, but that it could be the unintended consequence.

But I’ve said my part, so let’s get back on topic now 🙂

---

<div class="post-metadata">

**Author:** ![mikeshardmind](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/mikeshardmind/32/14381_2.png) [@mikeshardmind](https://discuss.python.org/u/mikeshardmind)\
**Post date:** [May 2, 2025, 1:24pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/36 "2025-05-02T13:24:16Z")

</div>

The current behavior of just assuming unreachable, and not requiring unreachable code be an error violates the gradual guarantee.

Requiring all unreachable code error will be rather noisy, contain false positives for places where people write “redundant” runtime guards, and require special casing of things like typing.asser\_never

The solution here follows logically, and there’s a means to detect only the cases that can _never_ be correct.

First, lets look at how this violates the gradual guarantee.

```py
def ex1(s: str, /) -> str:
    # this pattern for defaulting in data in the case of external data failures
    # has mistakenly inverted the condition. 
    if not isinstance(s, str):
        return s
    else:
        return ""

def ex2(s: str, /) -> str:
    if not isinstance(s, str):
        msg = f"Expected a str, got an instance of {type(s):!r}"
        return TypeError(msg) # should be raise, not return
    else:
        return s

```

In both of these cases, these violate the gradual guarantee. If the annotation for s is replaced with `Any`, we get “new errors” with current typecheckers.

While making all unreachable code an error would solve violating the gradual guarantee, it would make “correct” versions of the code above have false positives:

```py
def corrected1(s: str, /) -> str:
    if isinstance(s, str):
        return s
    else:
        return ""

def corrected2(s: str, /) -> str:
    if not isinstance(s, str):
        msg = f"Expected a str, got an instance of {type(s):!r}"
        raise TypeError(msg)
    else:
        return s

```

here, the checks the type checkers see as redundant cannot be provoked into letting an error case further into the program, so the “unreachable” code is benign. In both of these cases, swapping the annotation for s with Any, results in no errors.

Looking at the function “ex2”, here’s an example of the _actual_ logical statements, and why this doesn’t have to just be some heuristic function, but one that uses set theory to determine when unreachable code _cannot_ be benign, and can only function to cause error cases to further propagate.

1. We are in a typed context, but cannot know if all callers of the code are in a typed context. (This is because of python being gradualy typed)
2. We can know if everything we use within the function is typed or not.
3. We should only present errors we have evidence for.
4. Well behaved callers call it with a single positional-only argument that is an instance of a type that is a str or a subtype thereof.
5. Well behaved callers can never enter the branch that checks that s is not a str

Therefore, if we’re in a place where we have determined well-behaved callers cannot exist, we only have to concern ourselves with if the code is benign given calls that are outside of being “well-behaved”, if it isn’t, then we need to alert the function author that this code should be removed as it cannot have a purpose consistent with their type information.

Here, that’s looking at “what if our starting information for s is `~str`” (not a well behaved caller, so invert the overall function domain), in that branch, constructing `msg` is fine, even relying on the value of s, as we don’t have evidence this is an error, only that is is either unreachable or that s isn’t a subtype of str, however the TypeError there being returned is inconsistent with the return type (the corrected version correctly raises, and is fine), so this “normally unreachable” code can _only_ exist to be provoked into causing further inconsistencies.

Because we are in a typed context, we only examine for such errors with the not well-behaved calls branches that are reachable by not well-behaved calls, but are not reachable by well-behaved calls, preventing this from creating new errors for well behaved callers.

You can repeat this for all of the examples I’ve provided in this thread, as well as all of the versions I’ve said are correct.

---

<div class="post-metadata">

**Author:** ![mikeshardmind](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/mikeshardmind/32/14381_2.png) [@mikeshardmind](https://discuss.python.org/u/mikeshardmind)\
**Post date:** [May 2, 2025, 1:45pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/37 "2025-05-02T13:45:56Z")

</div>

To add onto the above, there’s multiple levels this can be addressed at to avoid violating the gradual guarantee, but leaving this as “no error at all” isn’t an option.

1. Inverting the function domain and examine if the places that should be unreachable can only exist to error further. This is the means that will error the least for unreachable code without violating the gradual guarantee.
2. ~~Within branches that are “unreachable”, error if this branch would be reached, assuming the type of the function inputs to be `object`, this will error more, but is a sensible, easier to implement method.~~
3. error for all unreachable code. This requires special casing assert\_never, as erroring for this would be in direct violation of why it was added.

I’m very positive on option 1 as it errors only for things that can _never_ be correct, I’m very negative on option 3, as it makes common patterns for sensible runtime guards a false positive.

edit: 2 doesn’t work in some cases where the type of a value is dependent on the type of an input

Each of the options here errors for all of the cases of the previous option, and then more.

For those who haven’t been following the current intersection draft closely, the inversion of function domains is a well-behaved operation that’s been discussed over there, but it _isn’t_ just inverting all parameters and calling it a day, it’s encapsulating all possible calls that are outside of well behaved calls.

So for `f(x: int, y: int)`, well behaved calls, x is an int and y is an int.  
the inversion here is: x is not an int or y is not an int (and that’s specifically logical or, rather than exclusive or)

---

<div class="post-metadata">

**Author:** ![Liz](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/liz/32/15021_2.png) [@Liz](https://discuss.python.org/u/Liz)\
**Post date:** [May 3, 2025, 7:00pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/38 "2025-05-03T19:00:09Z")

</div>

Just to clarify, are the below what you would expect for each case?

### Reachable as typed

- Assume the type information is correct, there’s no evidence to the contrary.
- Error if there’s an inconsistent use
- Unchanged from all current typechecker behavior.

### Unreachable as typed, unreachable even if function input annotations are replaced with Any

- Leave erroring up to typechecker/user-settings, this code can’t be reached even if it is called incorrectly, so it can’t cause problems by existing. May still be an error in that the author expects it to do something, but can’t ever.
- Unchanged from all(?) current typechecker behavior.

### Unreachable as typed, reachable if input annotations are replaced with Any

- Must error if when called wrong, it would do something that conflicts with other type information, as this can’t do what the user using a typechecker has expressed.
- Must not error if it would still continue to interact consistently with typed code, because the typechecker can’t guess that the user isn’t writing for the potential case where someone without a typechecker is using their code.
- Changed from all(?) current typechecker behavior

---

<div class="post-metadata">

**Author:** ![mikeshardmind](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/mikeshardmind/32/14381_2.png) [@mikeshardmind](https://discuss.python.org/u/mikeshardmind)\
**Post date:** [May 3, 2025, 7:02pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/39 "2025-05-03T19:02:01Z")

</div>

Yes, that’s an accurate summary for each case, though I expect that the logical statements above are more useful for actually deriving that all of those cases are statically determinable.

---

<div class="post-metadata">

**Author:** ![carljm](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/carljm/32/959_2.png) [@carljm](https://discuss.python.org/u/carljm)\
**Post date:** [May 4, 2025, 11:11pm UTC](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757/40 "2025-05-04T23:11:12Z")

</div>

> [@mikeshardmind](#):
>
> First, lets look at how this violates the gradual guarantee.
> 
> ```python
> def ex1(s: str, /) -> str:
> # this pattern for defaulting in data in the case of external data failures
> # has mistakenly inverted the condition. 
> if not isinstance(s, str):
> return s
> else:
> return ""
> 
> def ex2(s: str, /) -> str:
> if not isinstance(s, str):
> msg = f"Expected a str, got an instance of {type(s):!r}"
> return TypeError(msg) # should be raise, not return
> else:
> return s
> 
> ```
> 
> In both of these cases, these violate the gradual guarantee. If the annotation for s is replaced with `Any`, we get “new errors” with current typecheckers.

The first example doesn’t violate the gradual guarantee, at least not in mypy or pyright. Neither one emit any diagnostic on that code, whether `s` is annotated as `str` or `Any`. \[1\]

The second example violates the gradual guarantee if (and only if) a type checker silences all diagnostics in unreachable code. But whether a type checker should do that or not (in this example, pyright does not, mypy seems to) is not the same question as how it should handle `Never`; there’s no use of any expression typed as `Never` in the second example.

(I can offer some thoughts on the actual proposal, but the proposal still doesn’t seem clear to me, and reaching a common understanding of the motivating examples seems a good place to start.)

* * *

1. Pyright in strict mode emits some diagnostics if the annotation on `s` is omitted entirely, but those are opt-in diagnostics about missing annotations; they are designed to violate the gradual guarantee and not related to the discussion here.

[Previous page](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757.md?page=1)

[Next page](https://discuss.python.org/t/better-specification-for-when-the-presence-of-typing-never-should-be-considered-a-type-system-error/89757.md?page=3)