> in Idris
For a lower-tech approach, you can even do one in Standard ML[1,2], more or less in plain Hindley–Milner (no substantial use of modules). The error messages are admittedly miserable. Perhaps it would be more correct to call that one a type-safe middle ground between printf and std::ostream::operaror<<, though, and I have to admit that loses what for me is one of the principal advantages of (POSIX) printf: the format string is a string, so localization—which inevitably involves rearranging placeholders—is much easier.
It might be that the correct solution involves a string with placeholders, but with formatting instructions—and all dependencies on argument types—pushed outside (to the argument list or similar). I’ve toyed with something like that in C; unfortunately, it’s not as succint as normal printf unless I want to tie it to dynamic memory allocation. For C, there’s also the advantage that you can avoid pulling in floating-point formatting code if you don’t need it, without resorting to GCC-specific tricks like Cosmopolitan does[3], and that code is the biggest (code and data) space hog that keeps printf out of embedded and other kinds of lean programs.
[1] http://mlton.org/Printf
[2] http://mlton.org/Fold
[3] https://justine.lol/sizetricks/