MVP unification implementation plan
The implementation of unification (inference) following this document can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.
Stage 1: Type checker enhancement
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.
Stage 2: Global context enhancement
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.
unify as an extension of conversion checking. Add
UState and supporting functions etc.
Stage 3: Update the type checker to use
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).
Stage 4: Optimization
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