Correct me if I'm wrong, but you don't need to generate every permutation to determine whether or not a given union type can be passed into a method, right? If the parameter is of type `A | B` and the function takes `A | B | C`, you don't need to generate the whole space to determine that `A | B` satisfies `A | B | C`. Also, for v1.0 of the language, it doesn't seem like it would be a big deal to put the onus on developers to recast their `A | B` to a `A | B | C`.
It's not just about validating types. If B and C are implemented sufficiently differently, the compiler output for a function that takes (A|B) will be different than for the same function that takes (A|C), and both of those outputs can end up coexisting in the final executable. Unfortunately I don't know enough about the compiler internals to go into further detail.
As for manual recasting, sure, it's possible, but it's not a great tradeoff. Either you do type inference correctly and have developers crashing the compiler unless they recast their variables in seemingly arbitrary ways, or you cheat on inference and have developers getting "undefined method" errors on classes they didn't think they were using until they learn the rules. Ultimately it was decided that the latter was less common and easier to deal with in practice (just add a PlacentalMammal subclass to your class hierarchy that includes Cat and Dog but not Echidna). It's not a decision anyone is thrilled with but I think it's reasonable.
I guess "larger binaries at v1 but correct" and "slightly less ergonomic at v1 but correct" both seem like pretty good tradeoffs to my mind, but at this point we seem to be pretty deep into speculation.
