Partial type inference for dependent types I'm looking for resources on (partial) type inference for dependent types.

For example there could be a type inference scheme that fails if the term doesn't have a principal type, or a scheme that makes some choices and infers non-principal types.

I'm also not sure how to integrate type inference into constraint-based type checking.

Are there any papers on this?
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.