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.
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:
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.
- 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)
- We can know if everything we use within the function is typed or not.
- We should only present errors we have evidence for.
- 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.
- 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.
