Reduce complexity around ES and fully support the full calculus.
Context
This PR includes many changes, most of them have the same goal, achieve a more principal solution to inference and general typing.
I was too optimistic when I started working on ES + Locally Nameless as pointed out at #165, this turns out to not be a trivial problem and so I will be trying to develop a better intuition and write proofs for what should be possible.
This PR does:
simplifies the typed tree, dropping the TTerm / TType wrapper which are not currently used
add a printer for explicit substitutions, very useful while debugging
remove explicit substitutions from the typed tree, preserving them only on meta variables limiting
limit explicit substitutions to an inversible subset
Goals
Reduce complexity around ES and fully support the full calculus.
Context
This PR includes many changes, most of them have the same goal, achieve a more principal solution to inference and general typing.
I was too optimistic when I started working on ES + Locally Nameless as pointed out at #165, this turns out to not be a trivial problem and so I will be trying to develop a better intuition and write proofs for what should be possible.
This PR does: