  In this paper we describe how to leverage higher-order unification to type
check a dependently typed language with meta-variables. The literature usually
presents the unification algorithm as a standalone component, however the need
to check definitional equality of terms while type checking gives rise to a
tight interplay between type checking and unification. This interplay is a
major source of complexity in the type-checking algorithm for existing
dependently typed programming languages. We propose an algorithm that encodes a
type-checking problem entirely in the form of unification constraints, reducing
the complexity of the type-checking code by taking advantage of higher order
unification, which is already part of the implementation of many dependently
typed languages.
