There's ongoing work[1] on fixing that. Also let's see how migrating setoids to cubical type theory might fix more issues for Coq. Will they follow the Arend[2] path? That remains to be seen.

[1] https://github.com/coq/coq/pull/10764

[2] https://arend-lang.github.io/about/arend-features