You’re right, that line was sloppy and I’ve edited the post to fix it.
The module system can absolutely express value-dependent option types via config references. What I should have said is that it doesn’t lend itself nicely to formal reasoning about module composition, which you already noted. Two modules can each be internally consistent but break invariants when they merge. Today you catch that as a type mismatch error. The direction I’m interested in is whether you can state composition invariants as proof obligations in the kernel, so the failure is a rejected proof rather than a confusing eval error, and build those dependent module types from HOAS combinators so they compose by construction.
None of that is built yet, so the claim I made was both wrong on its face and a bad stand-in for the actual point. I’ve updated the post to say what I actually meant. Thanks for the correction.