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?