As a polarizing example—proof assistants use dependent typing. Their goal is to express interesting mathematical theorems as types and then finding typechecking

As a polarizing example—proof assistants use dependent typing. Their goal is to express interesting mathematical theorems as types and then finding typechecking programs constitutes as proof of those theorems. They absolutely want power and richness over inference---you probably wouldn't want to write a program with an inferable type anyway. It would be too boring.