Thanks for opening the discussion — and apologies, I should have been more explicit about what I’d like to get out of this discussion.
I agree that the most important thing is standardising the semantics of annotated symbols. With that in mind, it’s not currently specified what it should mean for a TypedDict to be marked as @final. See also final TypedDict · Issue #7981 · python/mypy · GitHub
If we decide that final TypedDict is not meaningful, I’d merge Ilya’s PR. If we decide it could mean something like “no extra keys” (either by deciding so or leaving it unspecified), then I’d worry more about the small soundness hole in Ilya’s PR, since users could have the expressivity to get the behaviour they desire more soundly. Ilya explains the soundness hole nicely here.
(If you’re missing background here, the discussion on the three linked issues is useful)
In that case, the secondary not-specification-related thing I’m interested in here is seeing what the community thinks of the soundness hole. Ilya pinged me several times on the PR asking for merge, and I usually don’t feel comfortable introducing unsoundness unless the community clearly desires it (and the relevant issues on mypy aren’t currently particularly popular).
To Eric’s general question, narrowing is definitely not nearly as important as standardising what annotations mean. There’s still some value in doing so and in particular there’s value in consolidating thinking about soundness holes, but I don’t think of narrowing as a priority for Typing Council