Fix effect substitutions, free names and unification of entities

[bugarela]

Hello

I finally figured out this substitution composition stuff! This should stabilize the effect checker a lot. Closes #1091 as a side effect. The main motivation for the fixes were problems encountered by @p-offtermatt (example in tests).

Turns out that substitution composition is really simple, and I was complicating it for the wrong reasons. As long as substitutions are properly applied to things before running unification on them, we can go back to the simple composition that we had at first, which is the normal thing from the papers.

This PR additions:

1. When trying to unify effect entities like [v0, v1, v2] and [v1, v2], instead of throwing an error because we don't do unification of sets, we simplify them to [v0] and [] which easily results in v0 |-> .
2. Free name tracking is now the same as the one for types, since I recently made advancements on the correctness of that. I just copied the code for now, we can try do to a generalization at some point.
3. applySubstitution is now called in two new places on inferring effects for applications, ensuring the effects being unified are both updated with the latest substitutions. This makes it so the substitutions resulting from unification can compose with the existing ones with the classic composition algorithm, and therefore I removed the extra complexity I had added to our compose (and to applySubstitutionsToSubstitutions).
4. applySubstitution was fixed, as it was not working properly for substitutions like [a |-> b, b |-> c].
5. internal fresh vars are now prefixed with underscore so they don't collide with the names generated while printing - this was causing bugs now that all the rest is fixed.

From this list, (3), (4) and (5) should also be applicable for types. I'll do that as a followup and check if it solves any of our open issues for the type system.

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[thpani]

Code LGTM! I have some more algorithmic questions though

[thpani]

Just to make sure: substitutions can never be cyclic?

Also, if not: do we really need to compute a fixed point here, or can we sort the substitutions topologically and apply them all at once?

[bugarela]

Just to make sure: substitutions can never be cyclic?

Nope, we check for cycles when generating substitution bindings.

Do we really need to compute a fixed point here, or can we sort the substitutions topologically and apply them all at once?

We could sort and apply all. Actually, I'm about 80% sure that we can assume that substitutions are already sorted topologically (because of the way they are constructed). However, I don't see a clear benefit of doing that over this? We are not iterating over all substitutions every time, we only call find - which sure, would be better in a simple array iteration, but then we have to worry about toposort.

[thpani]

However, I don't see a clear benefit of doing that over this?

idk, I'm always for avoiding recursion if things can be achieved in a single call.
I guess here the overhead does not matter much, because the arrays are small, but even so, small delays add up and I'd avoid them, especially for compile-time checks.

[bugarela]

Makes sense. I'll keep this for now and improve it a performance-focused pass in the future. There are way more pressing performance problems and, then, I'll find a way to be very careful to not make regressions with the optmizations.