Idris works by compiling the language to a fully specified intermediate representation that the checker acts on. The IR is described in a well-written publication and could fulfill the role of your suggested general checker. However, since proof checkers are relatively easy to write, most of the work being in the standard library, people don't seem to mind remaking them every time they design a new language.

The biggest advantage would be gained from increased interoperability between dependently typed language so that they could use each other's standard libraries, but the field may not yet be well-developed enough to standardize on basic definitions.