While dependent type inference is more difficult, you get program inference in exchange. That's not a bad tradeoff because I'd rather write the spec (type) and have the computer fill in the boring bits, rather than the other way around.

I remember seeing an Edwin Brady talk (it featured a now-possibly-famous Brexit joke) in which the compiler almost inferred ... I think it was either zip or a fold.