[Solved]: Generating constraints to solve dependently-typed metavariables?

A type checking system can be turned into a type inference system by making the rules linear and adding constraints.

I’ll use the application rule as an example. The checking rule in dependent types is this: $$frac{Gamma vdash t:Pi x:A.Bquad Gammavdash u:A}{Gammavdash t u: B[u/x]} $$ Linearizing this rule requires re-naming the 2 occurrences of $A$, such that we obtain: $$frac{Gamma vdash t:Pi x:A_1.Bquad Gammavdash u:A_2}{Gammavdash t u: B[u/x]} $$ But this isn’t correct anymore! We need to add the constraint $A_1simeq A_2$: $$frac{Gamma vdash t:Pi x:A_1.Bquad Gammavdash u:A_2}{Gammavdash t u: B[u/x]}quad A_1simeq A_2 $$ Note that $simeq$ denotes equivalence modulo your conversion relation ($betaeta$, typically), just like for the conversion rule, but it is now a unification constraint, since you may have meta-variables in your terms. In the course of type checking, you’ll accumulate constraints like these, to potentially solve them all at once at the end (or earlier for efficiency reasons). Now things can get trickier, because the type of $t$ itself could be a metavariable in context! A more generally applicable rule would therefore be $$frac{Gamma vdash t:Cquad Gammavdash u:A_2}{Gammavdash t u: B[u/x]} Csimeq Pi x:A_1.B, A_1simeq A_2 $$ Or alternatively, keeping the previous rule and adding the rule $$frac{}{Gamma_1, x:C, Gamma_2 vdash x: A} Csimeq A $$ at variable lookup time. Another useful remark is that in the checking system, the conversion rule only needs to be applied right before applications, and possibly once at the very end of the derivation. Since this rules correspond to a unification constraint in the inference system, this tells you where to place the constraints.