Partial type inference for dependent types
I recommend to look at (1) first, which might be the canonical early work on this problem and lead to the ATS programming language. (2) is a recent work on the same problem.

As to using constraints for type inference, (3) is probably the canonical reference.





H. Xi, F. Pfenning, Dependent Types in Practical Programming.
T. Terauchi, Dependent Types from Counterexamples.
F. Pottier, D. Remy, The Essence of ML Type Inference.