It appears like pyright and mypy are both ignoring the rules for type narrowing in the first example, and not narrowing this to Any & ~str in the first branch (it leaves it as just Any, which isn’t correct, and we have explicitly said how this kind of runtime narrowing should function in other parts of the specification, specifically while defining TypeIs), I expect that ty will error on that first one.
Well, part of the problem in demonstrating this seems to be that there’s multiple points of failure for typecheckers currently. I think @Liz 's summary may actually be a better place to start here.
The idea is to determine
Is the code reachable if called as typed?
If yes, only check as typed
If no, to determine if the unreachable code must be an error, determine if the code is inconsistent with the annotations when called as not typed. This limits the errors for this as “Normally unreachable, can’t serve a purpose that is consistent with the annotations, even for interaction with runtime checking of types”, meaning that there are no special cases needed for things like if TYPE_CHECKING (not reachable ever, so no errors for the other branch) or typing.assert_never (reachable only when called wrong, behaves consistently with every annotation)
As an aside, unless examining specific type checker behavior, I don’t think it’s usually useful to show what typecheckers currently do when looking to specify what should happen. It just leaves the discussion subject to determining if each part of the inference is correct in each typechecker.
Breaking this example down line by line, here’s what I expect from just theory, including my expectations on errors, and rationale:
def ex2(s: str, /) -> str: # no error
# no error, even though "redundant", runtime validation is valid
if not isinstance(s, str):
# expected inference of s: str & ~str OR Never
# conclusion: Unreachable, or combination of bad caller and s: ~str
# (called by a user from gradual/untyped code incorrectly,
# inverting function domain gives us the type(s))
msg = f"Expected a str, got an instance of {type(s):!r}" # no error
# error, returned rather than raised TypeError is inconsistent
# with the annotated return type,
# and this is reachable if s: ~str,
# detect and tell user to remove or fix the runtime guard.
return TypeError(msg)
else:
# expected inference of s: str
return s
def corrected2(s: str, /) -> str:
# no error, even though "redundant", runtime validation is valid
if not isinstance(s, str):
# expected inference of s: str & ~str OR Never
# conclusion: Unreachable, or combination of bad caller and s: ~str
# (called by a user from gradual/untyped code incorrectly,
# inverting function domain gives us the type(s))
msg = f"Expected a str, got an instance of {type(s):!r}" # this is okay with s: ~str
raise TypeError(msg) # this is consistent with the return type
else:
return s
@carljm here’s an example where both mypy and pyright break the gradual guarantee, but would error consistently if they followed what was here.
I’m using TypeIs to get away from both of the typecheckers special casing isinstance in a way incompatible with the current materialization rules for gradual types:
from typing import Any, TypeIs
def is_str(s: Any, /) -> TypeIs[str]:
return isinstance(s, str)
def breaks_guarantee(s: str, /) -> str:
if not is_str(s):
msg = f"Expected a str, got an instance of {type(s):!r}" # no error
return TypeError(msg) # no error
else:
return s
def breaking_guarantee_now(s: Any, /) -> str:
if not is_str(s):
msg = f"Expected a str, got an instance of {type(s):!r}" # no error
return TypeError(msg) # error
else:
return s
What’s proposed here is also consistent with the proposed handling of Never in Intersections and how we are able to distinguish attribute presence from attribute type.
I’m hesitant to change this to “specifying error conditions for unreachable code”, because while that covers these examples, it doesn’t generalize to what we need for intersections as a whole.
Flags have been raised on this topic expressing frustration at how the conversation is going. It doesn’t seem like anyone is reaching consensus, and are instead arguing in circles or not understanding each other. Many long replies with multiple points are being posted, which makes it hard to follow or respond productively. Keep in mind our participation guidelines, including:
Avoid overwhelming a conversation and leave room for other voices. Be aware of the number, length, and frequency of your posts compared to others in the topic. It can be difficult for others to participate if a few voices take up the majority of a topic.
Do not respond to every post. Decide what avenues to focus on and which are distractions. Be concise. You can make your point in one or two posts, repeating the same arguments isn’t productive. Trust others to see your post and consider it along with the rest of the topic.
If you disagree with something, state your point and move on. You do not need to have the last word. Not responding, and letting a discussion naturally conclude, is often the better decision.