Or at least, I think that's probably a fundamental underlying model. There's a lot of higher level clever things that Nim does before getting to separate C files, I think separate .c units is just an optimisation not a restriction, but that it did to some extent shape how the Nim compiler logic worked during development.
Nim probably just needs to be taught to be able to treat "let x = 5.Foo" and "let x = 5.toFoo" the same way, rather the base case of how separate C compilation works. In which case, types.o in the not-working version still wouldn't export any (proc) symbols, but lib.c would know that it was dealing with an int. I think it might be something like a small bug or limit on the type inference, where technically it could infer something, but it's not yet able to. Well, basically I think it's something like there's no huge formally unifying theory behind how the entire Nim lang semantics should work for a given lang ver (eg, something like a lang report spec made by committee); but rather it's something that's defined by what the most recent compiler supports, as well as Araqs insights over time.
