I agree that the original wording was incorrect, but I find the new wording to be confusing because it justifies assignability only for "two fully static types". Assignability should not depend on whether either type is fully static; it should work fine for any gradual type. Maybe it's best to simply delete the preamble of this sentence (the part before the comma) and simply state that "type[B] is assignable toTypeForm[A] ifB is assignable toA".

My thinking here was that subtyping is the more "fundamental" operation; assignability follows from subtyping plus materialization. In particular, from the sentence I wrote plus the definition of assignability, your sentence follows, but not the reverse.

Ah, I understand your thinking. If a subtyping rule is defined, then assignability rules are implied by it.

This section in the PEP is named "Assignability", so I guess I was expecting to see assignability rules. Your point is that the assignability rule is implied, but it might be best to spell it out here in addition to the subtyping rule.

We seem to be inconsistent in the spec currently. In most places, we spell out assignability rules without talking about the underlying subtyping rules. For example, the Callables chapter has a section namedAssignability rules for callables, and it doesn't talk about subtyping. Same withTypedDict. But in thetuples chapter, we talk more broadly about "type compatibility rules" and do mention subtyping.

I don't have a strong opinion here, so I'm OK if we stick with your proposed wording.

Yes, I think we have more work to do to make the spec more consistent.

One way to sidestep discussion of the nuances of "fully static types" here, while still being correct, would be to say that for any two typesT1 andT2 whereT1 is a subtype ofT2,TypeForm[T1] is a subtype ofTypeForm[T2].