But how does it know to do this just by unifying the types enum(?0, ()) and enum(i32, ())?
Why would it not choose ?0 = i32?
Kind of, although I picture it happening in the other direction due to the in-order nature of the type checker. i.e. at the point that it unifies enum(?0, ()) with enum(i32, ()), it needs to produce a "nondeterministic" result that ?0 is somehow either enum(i32, ()) OR i32.