Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work.
The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables.
Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
