Partial type inference for dependent types

Question

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?

Answer 1

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.

---

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