[red-knot] Gradual forms do not participate in equivalence/subtyping

[sharkdp]

Summary

This changeset contains various improvements concerning non-fully-static types and their relationships:

• Make sure that non-fully-static types do not participate in equivalence or subtyping.
• Clarify what Type::is_equivalent_to actually implements.
• Introduce Type::is_fully_static
• New tests making sure that multiple Any/Unknowns inside unions and intersections are collapsed.

closes #14524

Test Plan

• Added new unit tests for union and intersection builder
• Added new unit tests for Type::is_equivalent_to
• Added new unit tests for Type::is_subtype_of
• Added new property test making sure that non-fully-static types do not participate in subtyping

[github-actions]

ruff-ecosystem results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

[carljm]

This is fantastic. Super clear and correct. Thank you.

[carljm]

I think for these three, we also need to check the MRO for an Any/Unknown base? A class that inherits Any/Unknown is not a fully static type.

[sharkdp]

Yes, thanks!

For Type::Instance(_), this is obviously correct.

For Type::ClassLiteral(_) it took me some time to understand whether we want that or not. I had a good discussion with @AlexWaygood and I believe I now understand why we want that. This also seems to match mypy's and pyright's interpretation:

from typing import Any

class FullyStatic: ...

#instance1: int = FullyStatic()  # obviously doesn't work
#class1: type[int] = FullyStatic  # same

class Gradual(Any): ...

instance2: int = Gradual()  # okay, `Gradual` is a gradual type
class2: type[int] = Gradual  # also okay

I then went on to implement this, which seemed fairly trivial at first. But it turns out that this causes all sorts of problems. One of these problems is that we don't fully understand even the most basic types like str. In typeshed, str inherits from Sequence[str], which is a complex generic protocol. This currently manifests in the following MRO for str, which causes us to believe it would be a non-fully-static type.

tuple[Literal[str], Unknown, Literal[object]]

This can be patched by matching on a set of known classes. But that is far from ideal. If someone unknowingly pulls in another type from the standard library (outside the set of known classes; see #14769 as an example) with a similar problem, they would see all sorts of weird behavior without a clear indication of what's wrong.

And then there is also another problem where merely iterating over the MRO of a class here (without drawing any conclusions from it) causes us to eagerly infer some types as Unknown.

If someone has a good idea on how to resolve this (right now, without waiting for generics), please let me know. Otherwise, I would suggest we move forward with the TODO comment and revisit this when we understand generics.

For reference: here is what I tried: ec64bd8

[carljm]

Fully agree with this analysis and I think the conclusion is right; we need to defer this handling until we can understand most/all typeshed classes that aren't supposed to inherit Any/Unknown, as not inheriting Any/Unknown. TODO comment (and maybe an issue on the backlog, too) seems the right move.

[carljm]

This is a bit scary :/ It suggests we frequently need to ask about the fully-static-ness of a type too soon. I guess we'll cross this bridge when we come to it; hopefully we can find a way to defer the need for checking this so early.