To be sure I understand correctly, every defs of each source file would be written to a unique "output" file (which would be read as if there was only one file).
No. The idea would rather be to write into a file a "tuple" containing the few definitions you want to export from the file (i.e. those that are visible from outside). I.e. one source file turns into one "compiled" file.
Isn't it a waste of time to write and read to/from a "output" file (in other word, couldn't it be done in memory instead of on the disk) ?
It gives you a limited form of separate compilation (the "compiled" file has already been elaborated, so you don't need to macro-expand its code any more nor do you need to do any kind of type-inference).
Stefan