I think it would be worth mentioning that in normal use (strict mode) Pyright simply requires you to add type annotations to the declaration. Occasionally mildly annoying but IMO it's clearly the best option.
I don't enable strict mode on multiple projects because people don't want to type anything outside of function signatures.
Inferring the type from the first use is 100% the correct choice because this is what users want 99% of the time, for the rest you can provide type information.
things: set[tuple[str, str, int]] = set()
users: list[User] = []
In fact, I recently migrated a project from Pyright to Pyrefly for performance reasons, and there was very little I had to change between. The most annoying thing was Pyrefly's lack of exhaustive pattern matching for StrEnum and Literal[...]
> To improve type safety in these situations, type checkers that infer Any for empty containers can choose to generate extra type errors that warn the user about the insertion of an Any type. While this can reduce false negatives, it burdens developers by forcing them to explicitly annotate every empty container in order to silence the warnings.
ie: "type checkers that don't infer container types can emit an error and require users to annotate"
If the type checker can infer a type then the annotation would only be required if the inferred type doesn't match the user's intent, which means one would need to add fewer annotations to an arbitrary working-but-unannotated program to satisfy the type checker.
Adding explicit types strategically (e.g. in function signatures) tells the compiler (and readers) explicitly what the type should be, so if you add code that violates that it gives you an error instead of silently inferring a different type.