Finals and Literals: Spec contradiction

[srittau]

This came up in python/typeshed#16301. I assume this is mostly a clerical/historical error, but let me know if we should follow the whole spec change process.

---

The typing spec says about Final:

Example:

ID: Final = 1

The typechecker should apply its usual type inference mechanisms to determine the type of ID (here, likely, int).

And then a bit later:

Type checkers should treat uses of a final name that was initialized with a literal as if it was replaced by the literal.

Both sentences are copied directly from PEP 591, which overlapped with the Literals PEP 586.

I assume that we should change the first sentence to "here, likely, Literal[1]" and change the second sentence to be a bit more concrete along these lines:

Type checkers should infer uses of a final name that was initialized with a literal X as Literal[X] if X is an allowed literal type (cf. to the literals section). Otherwise, they should infer the type of the X.

(And maybe extend the example after a bit.)

In fact, this is what the conformance tests already check:

typing/conformance/tests/qualifiers_final_annotation.py

Lines 11 to 13 in cf943cc

	ID2: Final = 1
	assert_type(ID2, Literal[1])

(Although the tests could be extended a bit.)

[carljm]

I do think a clarification to the spec text is warranted here; the current text is confusing. I think we should remove (here, likely, int) and instead mention the later "replacement" rule. And we should probably also clarify that the replacement rule applies to a bare Final annotation with valid literal initializer.

I would consider this a spec clarification, not a change in specification.

[srittau]

As @carljm points out in #2352, the Literal section of the spec has a whole section about the interaction with Final that actually is already correct. We should probably just change the mentions in the Final spec part to point to that section.