Great write up, and you're absolutely right that implicits are moving towards ML modules. Quite possibly a production system would end up being synonymous with ML modules out of the need for named impls.

Small nit in terminology, the implicits described are coherent. Part of their value over previous implicit work is that they are coherent and stable. I have generally seen the property you're referring to called canonicity, which they do lack.