I might be missing context here but the fact that type systems are logic languages should be uncontroversial given that that's what the Curry Howard Correspondence is about. Though I'm not very well read I think that using "complete" generic logic languages/solver (as a component) in solving type equations ought to be well trodden ground, my first thought went to https://github.com/rust-lang/chalk as one example. I'd be looking at what one might give up doing so as the reason why it doesn't happen more: speed? guaranteed termination? good error messages?

I do think something like prolog might not be fit for it as the error messages seem poor, but it feels like a solvable problem - something like a stack trace instead of the "no" that prolog can give.