> Nah. Both Prolog and C do a very similar step: they walk through call-sites and function signatures in your code and check them for compatibility with each-other in a way that can constrain both the call and the function,
C type checking does not "constrain the call and the function". It looks at existing, fixed types (not constraints on types) and fails or succeeds. I may be misunderstanding you, can you explain in more depth what you mean?
> or they fail to make a match and they rewind and try again with other constraints.
I don't think C compilers ever backtrack during type checking. Again, maybe I'm misunderstanding what you mean?
> The only difference is that C is only doing this unification for the types of the parameters, whereas Prolog is doing it for the parameter values.
Other big differences include the fact that the C compiler does this at compile time as a preparation for execution, while in Prolog this is most of execution; the fact that Prolog has logic variables; the fact that Prolog has arbitrary nested structures that can be unified; the fact noted above that Prolog does backtracking; and, in general, the big difference that Prolog is nothing like C at all.
> Any programming language that has static types but also has an “auto” variable type, where the type is deduced from the use-def and def-use chains that statement live in, is doing absolutely everything Prolog does, and just not exposing the power of it to you. (Hindley-Milner is an even more advanced constraint-solver than Prolog is.)
AFAIK plain Hindley-Milner does only unification but not backtracking, so I would call it strictly less powerful than Prolog. If we assume a backtracking version of Hindley-Milner, we might call it equally powerful to Prolog. I don't see at all how you can claim that it's "more advanced" than Prolog, though.
> (Though, to be clear, if you can program in the type system, as you can in C++, then you do get an exposure to that power, and can write many backtracking algorithms with it.)
I don't know enough about the intricacies of C++ template metaprogramming, but I'm not under the impression that it exposes backtracking as a primitive the way that Prolog does. (Modulo the trivial observation that C++ templates are known to be Turing complete, so you should be able to implement your own backtracking in them.)