Are there any real world online resources where, modulo redirect, a different resource is presented on the HTTP and the HTTPS protocols? Or alternatively, on ports 80 and 443?

There used to be, though it's less true now. However, the reason to treat them distinctly (as different origins, technically) is that HTTPS provides integrity whereas HTTP does not. So, consider the case where the client enters an HTTP URL and is redirected, just as you say above. If the attacker injects their own JS and it is cached in an origin that is just `example.com`, then they control the user's experience of the site, even if later the user securely goes to the site with HTTPS.

Thank you. That really is a novel attack that I didn't think of.