Isn't that a non-extensible built-in that's handled "magically" by the compiler? (Apologies if that's wrong, it's been a few years since I've used O'Caml.)
In Idris it's possible to write a type-safe printf entirely in library code -- no magic.
That's the "magic" being discussed, where the value determines the type of something, hence, dependent typing :)
The magic that's happening in the ocaml compiler isn't dependent typing - it's a purely syntactic transformation, something like GHC turning "hello" into ['h', 'e', 'l', 'l', 'o'] into 'h':'e':'l':'l':'o':[]. ocaml notices that you have a string literal in a place where a format string is expected and swaps it out - that's all. It's magic, but it's unrelated to the type system - the type system comes in later.
What does it replace it with? A value of type ('a, 'b, 'c, 'd, 'e', f) fmt. fmt is a GADT [1], fully defined within ocaml [2] - and I promise, ocaml does not have full dependent types.
[1] https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ...
[2] https://caml.inria.fr/pub/docs/manual-ocaml/libref/Camlinter...
ATS is essentially 'C with dependent types'. And optionally some other languages with dependent types. You can think of its dependent type checking and theorem-proving as 'pre-compilation', since there's no runtime overhead to it (and since you can separate it out into its own compilation step, including swapping out alternative solvers). ATS's relationship with C is good enough that you can take an arbitrary C program and start tightening its screws by injecting a bit of ATS into it.