Runtime error that type checks. Is this a bug? #11436
Replies: 1 comment
Pyright Discussion Answer: Runtime Error That Type ChecksShort AnswerI think this is an unsound narrowing case caused by overlapping union members, not a runtime bug in At runtime, isinstance(Violation(3), Left) # True
isinstance(Violation(3), Right) # TrueBecause case Left():
return handle_left(value.value)So type Either[L, R] = Left[L] | Right[R]For this specific call, the type checker can accept Why the Narrowing Is UnsafeThe unsafe static step is the narrowing from: Left[L] | Right[R]to: Left[L]inside the That narrowing is only sound if Violation[T] <: Left[T]
Violation[T] <: Right[T]A fully sound narrowing would need to preserve that overlap. Conceptually, the Left[L] | (Left[Any] & Right[R])or in this specific call: Left[str] | (Left[Any] & Right[int])But Python's type system does not have general intersection types or sealed/disjoint class hierarchies, so most type checkers pragmatically narrow as if the union arms are disjoint. That is useful in normal code, but it becomes unsound when union members can overlap through subclassing. Practical Fix 1: Make the Variants FinalThe cleanest static fix is to make the variant types disjoint by design. If subclasses should not exist, mark the variants as from dataclasses import dataclass
from typing import final
@final
@dataclass
class Left[T]:
value: T
@final
@dataclass
class Right[T]:
value: TThat should make this invalid to a type checker: @dataclass
class Violation[T](Left[T], Right[T]):
value: TThis is probably the right model if Important Runtime Note About
|
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
The code below type checks in pyright, but produces a runtime error where
assert_neveris called.Code sample in pyright playground
It is unsafe to narrow
Left[L] | Right[R]toLeft[L]in the Left match arm without considering the possibility of overlap betweenLeft[Any]andRight[R]. I suppose it should be narrowed to something likeLeft[L] | (Left[Any] & Right[R])if python had intersection types.I wonder if this is a known limitation of python's type system. It would be rather inconvenient if one had to mark every class with
@finalif one wanted type checkers to narrow in match arms.This also type checks in ty, mypy, and pyrefly, but ty and pyrefly require a bit more persuading to accept the code: Code sample in ty playground. Code sample in pyrefly
All reactions