The spec currentlydefines materialization as follows:

Given a gradual type A, if we replace zero or more occurrences of Any in A with some type (which can be different for each occurrence of Any), the resulting gradual type B is a materialization of A.

A typeA is assignable toB if there exists a pair of materializations A' and B' of A and B such that A' is a subtype of B'.

Now let's consider whetherlist[int] | list[str] is assignable tolist[Any]. To do so, we have to consider materializations oflist[Any], created by substituting Any with some other type. But there's nothing we can substitute for Any that would make for a fully static type that is a supertype oflist[int] | list[str], sincelist is invariant in its type parameter. Therefore,list[int] | list[str] is not assignable tolist[Any]. Relatedly, this meanslist[Any] | list[Any] is not equivalent tolist[Any]. This is obviously not a desirable conclusion; current type checkers treatlist[int] | list[str] as assignable tolist[Any], and they should.

I think to fix this, we could say that ifA' andA'' are materializations ofA, then the unionA' | A'' must also be a materialization ofA.