I've managed to build MicroPython in native esp-idf way, as esp-idf component. Pycom's MicroPython could be possible adapted to the same build system.
It works very well, no more manual sdkconfig.h tweaking is needed, MicroPython options can be configured from menuconfig, ESP32 can operate in unicore or dualcore mode, SPI Flash can operate in any mode and speed supported (QIO, QOUT, DIO, DOUT; 20/26/40/80 Mhz), many things works better because it is build as it should (from esp-idf's point of view).
psRAM is also suported (It is huge difference between MicroPython running with less than 100KB of free memory and running with 4MB of free memory.).
The project is available on GitHub.
Tested on ESP-WROVER-KIT with ESP-WROVER module with 4MB psRAM.
After two solid says of trying to debug the modified SD over SPI driver, it turns out that there is a bug in the SPI class (see this post). After rewriting the driver to use only the write_readinto function, along with a dummy buffer filled with 0xFF, all of my test SD cards worked perfectly. What probably delayed me discovering this low-level issue is that a few of my test SD cards did work, but many did not, with a wide variety of failure modes. Clearly, sending 0xFF is a requirement, but apparently there are some SD cards that are tolerant of getting other values (like 0x55 in this case).
The resulting code is fairly ugly right now. I'm hoping that the SPI class issue can be resolved quickly, at which point, I'll go back and test that version of the code.
By the way, the original SD over SPI driver uses this syntax for SPI read functions: read(1, 0xff). This results in an error (extra positional arguments given); the documentation says to use: read(1, write=0xff). This is accepted, but the 'write' argument is ignored.