I think in dependently typed programming languages and theorem proves. As I understand it, even System F (like Haskell) benefits, no?

I guess in System F, if a function f accepts a complex type A, and another function g returns a complex type B, both types could involve type variables. Then for the compiler to check whether the expression f(g) is valid, it (the compiler) needs to determine whether a unification of A and B is possible. Not sure though.