When do type systems start needing a logic engine?
I'm not sure where you would draw the line between "direct type checker" and "logic engine". In a deep sense every type checker for a modern type system is a theorem prover (or proof-checker; more on this in a moment). The theorem to be proven is "the program is well-typed", or "this function has type X".

Modern type systems and their checking/inference algorithms tend to be specified in terms of logic; typically intuitionistic typed logic (a.k.a. Martin-Löf theory). If you have a look at, say, the paper for the standard Hindley-Milner type inference algorithm [1], you'll see that it's specified abstractly in terms of logic. Let-polymorphism also relies on the Robinson unification algorithm, famously used in Prolog.

I'm going to go out on a limb here and suggest that the degree to which a type inference algorithm resembles a "logic engine" (however you define it) depends on how "decidable" the rules are, and how much "inference" you need to do (as opposed to merely "checking"). The type system of the simply-typed lambda calculus is intuitionistic logic (and I do mean it really is the same thing; this is the famous Curry-Howard correspondence), so you'd think that any type checker for that system is a "logic engine" in any reasonable sense. But because you only need to "check" rather than "infer", it's a proof checker rather than a theorem prover.

The standard introductory reference on this topic is TaPL [2]. If you're at all interested in this topic, it's well worth a read; any well-stocked university library should have a copy.




Principal type-schemes for functional programs by Damas and Milner (1982).
Types and Programming Languages by Benjamin C. Pierce.