Currently Teika handles in many places both locally closed types and non locally closed ones. This makes so that whenever a unification variable is created the compiler needs to "guess" which kind of variable it will be. Additionally some substitutions cannot compose due to that.
While this may be desirable in the future for performance reasons it drastically increases the complexity of the typer, so in this PR, I make sure that every typed term is in the locally closed form.
This breaks typing for self types, but those will be restored very soon.
Goals
Simpler inference algorithm.
Context
Currently Teika handles in many places both locally closed types and non locally closed ones. This makes so that whenever a unification variable is created the compiler needs to "guess" which kind of variable it will be. Additionally some substitutions cannot compose due to that.
While this may be desirable in the future for performance reasons it drastically increases the complexity of the typer, so in this PR, I make sure that every typed term is in the locally closed form.
This breaks typing for self types, but those will be restored very soon.