At compile-time, sure. But ML-like languages in general have no support for runtime logical programming. They don't provide an API to do things like type infere

At compile-time, sure. But ML-like languages in general have no support for runtime logical programming. They don't provide an API to do things like type inference at runtime. For a good reason too, the only possible way type inference in ML-like languages work is because the computational cost is abstracted away from the runtime. Logical programming (ala Prolog) is very useful but the truth is it's asymptotically inefficient. Standard ML's type inference algorithm was, for example, asymptotically exponential. It just so happened that for useful programs it halts in a reasonable amount of time. This is not something you can provide an API for so that at runtime you can run arbitrary type inferences.