I'd like to propose adding two new type constructors, ty_extensions.Top[T] and Bottom[T]. Top[T] represents the top materialization of T, the smallest type that is a supertype of all materializations of T. Bottom[T] is the bottom materialization, the largest type that is a subtype of all materializations of T. These types would be exposed in ty_extensions for testing, and ty would synthesize them internally in some circumstances.

There are a few possible use cases for these types:

• isinstance() with generic types (Support isinstance narrowing of specialized generic classes #456). For example, isinstance(x, list) could be implemented like TypeIs[Top[list[Any]]].
• A more elegant implementation of various operations on gradual types, such as assignability and equivalence (Consider using top / bottom materialization for assignability check #666). A assignable-to B can be implemented as Bottom[A] <: Top[B]; A equivalent-to B is Top[A] = Top[B] and Bottom[A] = Bottom[B]. In general, the top/bottom materialization allows you to transform operations on gradual types to operations on fully static types.
• The top and bottom materializations also show up in some approaches for implementing operations on intersection and negation types, as I discussed for negation types.
• Top[T] could potentially become part of the "public" type system later (i.e., something users would be expected to write in their own code). For example, it can be useful to express that a function accepts any instance of an invariant generic type, regardless of the generic parameter. (Not so much for Bottom[T]; I have a hard time coming up with uses for that as a public type.)

There's also some risks:

• It may hurt performance to create more complex implementations of common operations like assignability. Perhaps caching could help.
• But if we add caching, it may also hurt memory usage.
• Error messages may get worse if we're not careful, since we might end up exposing internal-only Top and Bottom types that confuse users.
• There are some theoretical issues with these types in the context of Python's type system. It may be possible to work around these issues and end up with something practically useful, but it's also possible that these issues mean that the idea doesn't work out in practice. In particular:
  • The bottom materialization doesn't fit well in a set-theoretic formulation of Python's type system, because in many cases (such as Bottom[list[Any]]) it's logically equivalent to Never, as there is no value that is a member of Bottom[T]. However, if we actually reduced these types to Never, assignability wouldn't work the way we'd want. So we have to treat Bottom[list[Any]] as an irreducible type and define how things like subtyping work on it. My intuition is that it's possible to do this in a way that ends up with a sensible set of results, but the theoretical foundation is shaky.
  • Top[T] for a fully static type is the same as T, but what is a fully static type? There's reason to say that if any attribute on a type T is a gradual type, then the value of that attribute on Top[T] is the Top of that gradual type. If we don't do this, then subtyping between protocols and nominal types might not behave quite correctly. But object contains Any in several of its attributes, so does that mean Top[object] is a distinct type that is a supertype of object? I am not sure yet if there's a good solution here.

Given those risks, it's somewhat speculative whether this project would actually work out, but I'm interested in working on it and seeing if I can make it work. Let me know if you think it's reasonable to try it out!

My plan would be along the following lines:

• Do some more thinking about the theory behind this, particularly the issue listed above about Any inside nominal types.
• Add new type variants for Top and Bottom, and fill in basic scaffolding for them.
• Implement the necessary operations on top and bottom types, such as:
  • Simplification (e.g., Top[Top[T]] = Top[T]).
  • Subtyping
  • Attribute access
  • Disjointness
• Start using Top and Bottom internally for implementing other operations
  • For assignability, run both this and the current implementation and see if they match