Source-tracking unification

We propose a practical path-based framework for deriving and simplifying source-tracking information for term unification in the empty theory. Such a framework is useful for debugging unification-based systems, including the diagnosis of ill-typed programs and the generation of success and failure proofs in logic programming.