The implementation of unification (inference) following this document can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.
At the time of writing, the first stage of the totality checker MVP is finished. But the second and third stages, namely type checking data type and function declarations are required before unification can be implemented.
At the end of this stage, conversion/type checking for constructors is implemented.
Hole and Guess should be added to our global context for meta-variables. We may want to parameterize our global context constructors more heavily like in Idris 2 to avoid mistakes.
Implement functions unify as an extension of conversion checking. Add UState and supporting functions etc.
Implement newMeta and newConstant.
typeTerm should call unify instead of the conversion function. During type checking, when we encounter an Implicit, we make a meta-variable with the expected type, and hope that unifying the meta-variable and the expected type will succeed. (See the last part of the Unification in Idris 2 document).
We may need to reduce the time it takes for unification to finish. It could be rather slow. We could implement optimization tweaks to improve efficiency. For example, when do we call solveConstraints? Calling it at strategic times can improve efficiency dramatically. Can we compare terms in some circumstances without converting them to Value?