Thank you for the excellent summary! I found this much clearer than the presentation in the previous thread, and very easy to understand.
I would like to suggest a slightly different theoretical foundation for the understanding of Any [1], which I think can help inform this decision. In particular, I think it helps frame options 2 (and to a slightly lesser extent, 1) as less of a special case; rather, they are consistent with our usual understanding of Any.
I don’t think that Any is ever “the top type” in the Python type system. The top type is object. In a set-theoretic treatment of types, the top type is “the set of all possible values.” In Python, this is object. In a static type system, the top type is not “compatible with any type.” In fact, it is compatible with no type at all, besides itself.
Any is, in contrast, not “the set of all possible values”, but some particular (and likely limited), but statically not known, set of values. This is the interpretation that allows Any to be compatible with any type, and to have any attribute or method. When a type-checker sees an attribute access on a value typed as Any, it should say “oh, Any here represents some set of values which all have that attribute,” and not throw a static type error.
The purpose of Any in gradual typing is to allow interoperability with statically-untyped code, where the code author takes responsibility for correctness, without having to deal with false positives from a static checker’s lack of knowledge. Thus, type checkers should generally aim for the most “favorable” (i.e. not-false-positive-causing) interpretation of Any.
IMO the option that best meets this criterion is “LSP-compatible Any,” and the second-best is “Any that always prioritizes known attribute types.” I think “pure Any” is not actually a pure interpretation at all, but a misunderstanding of EDIT: this conclusion isn’t quite right. All three proposals are consistent with the above understanding of Any.Any, and “pure Any” goes the furthest in making the “most favorable” interpretation. But the above understanding of Any also gives us freedom to choose a slightly more restrictive interpretation of what sets of values Any can represent in a particular situation, if we judge that some additional assumptions greatly reduce false negatives with a small cost in false positives. And in this case I think assuming LSP compatibility fits that bill.
So I don’t think that this is how we should approach option 1 or 2; rather, we should give a clearer definition of Any (as described above), which is already (and always has been) different from “the top type,” and is already consistent with these options.
[1] Full credit to @kmillikin for this definition of Any in his earlier work on a from-scratch specification for Python typing.