Hindley-Milner style type inference, which is done by MLs and is similar to what is done in Haskell, uses unification, which is a large part of how Prolog reaso

Hindley-Milner style type inference, which is done by MLs and is similar to what is done in Haskell, uses unification, which is a large part of how Prolog reasons, to determine if two types with still unknown subparts can be the same. You can do surprisingly complex things in these type systems. For a more complex type system that does similar things and allows a lot more reasoning in the type system, you could take a look at Agda. This is a Haskell-like language with a fully dependent type system, i.e., types can contain arbitrary language terms. This has the downside of being not-quite-Turing-complete, as you want to be able to decidably typecheck. However, it is powerful enough that its type system is often used to automate proofs about both programming language theory and more ordinary math.