As I understand it, dependent type theory requires higher order unification, which is undecidable. So they typically use bidirectional type checking instead of Hindley Milner.

With bidirection type checking, I think it only needs the unification when solving inserted implicits. So a plain dependent type theory wouldn't need it, but once you add implicit parameters, you do need it. They usually use pattern unification, which solves a subset of higher order unification problems, for those unification problems.