Prepare for higher-order unification and clear the typing substitution pipeline.
Context
My current design for doing higher order substitution will be to accumulate all the substitutions in the context, then invert them before unifying.
Currently the typer first emit open terms and then close them later, while this works, a possibly more interesting approach is to emit the closed terms and register a substitution to keep them open while typing, due to that terms are automatically closed when it is over.
This is probably slower due to accumulating too many substitutions but this can be mitigated with better data structures easily in the future. Additionally it makes let aliasing quite straightforward(just one open).
Goals
Prepare for higher-order unification and clear the typing substitution pipeline.
Context
My current design for doing higher order substitution will be to accumulate all the substitutions in the context, then invert them before unifying.
Currently the typer first emit open terms and then close them later, while this works, a possibly more interesting approach is to emit the closed terms and register a substitution to keep them open while typing, due to that terms are automatically closed when it is over.
This is probably slower due to accumulating too many substitutions but this can be mitigated with better data structures easily in the future. Additionally it makes let aliasing quite straightforward(just one open).