> The more expressive a type system is, the more difficult type inference becomes.

This is always mentioned and I always fail to see the relevance. Inferable terms stay inferable when we add dependent types.