There exist several microkernels that don't suffer much from overhead, it's not hypothetical but decades old technology, from oldest to newest: QNX, the L4 family, Fuchsia, RedoxOS.
Yes, but they remain confined to niche applications because none of them has been designed to be incorporated in a framework that would allow the gradual migration to them of the legacy applications and device drivers.
Only Fuchsia might have a chance, because of the disproportionate control that Google has over the Android applications and because of the constraints imposed on those.
Fine by me. Technology-wise, it doesn't seem to do anything cool that hasn't been done before, and its business goals seem to be to get rid of that pesky GPL2 licensed stuff and to introduce a stable ABI for drivers (i.e. no accidental drivers for "real Linux" because of Android anymore).
I spent a lot of time with Minix 3 (see https://github.com/rochus-keller/Minix3/tree/Minix3_Book_TCC). The intention was to make the book version compile with TCC. It turned out that this version only covers a fraction of the relevant parts necessary to build a working system. Minix 3 in addition includes hundereds of assembly files. The impression created by the book of a lean C implemented kernel, or the claim "for compiling a small Minix system" are wrong. Not even the kernel is complete; the central IPC is actually implemented in assembler and linked with the kernel via some library not described in the book.
The reason why I omitted Minix is that I don't know about its performance characteristics. Same for TRON / eTRON which is or used to be huge in the Japanese industry.
Only Fuchsia might have a chance, because of the disproportionate control that Google has over the Android applications and because of the constraints imposed on those.