Remove erroneous occurs check from "effect entity" unfication

[shonfeder]

Closes #1356

The originating issues was caused by fairly subtle error in our unification algorithm for the effect checker, which was making an invalid occurs check. This error was hard to spot, because (I think) we are not used to thinking of unification sets! I think we usually think of unification in terms of the "geometric structure" of the syntactic terms being unified. E.g., when unifying lists, [A, B] =.= [C, D] iff A =.= C, B =.= D, and A =.= [1, 2, A] should fail an occurs check because it would require unifying A with a term that includes itself as a sub-term. However, the extensional nature of sets invalidates the "evident" geometric intuition that guides us in the previous examples. A =.= B ∪ C ∪ A is true iff B =.= C =.= A.

This is also explained in a bit more detail in comments added with this change set.

The PR also includes a regression test and some simplification of the effect inference code, introduced during the debugging process.

• 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

[bugarela]

Don't we need to check if name === entity.name here to avoid cyclical bindings?

[shonfeder]

I don't think so. a =.= a is ok. It just unifies to an empty substitution. Cyclicality is only a problem when a variable is to unify with a term that includes itself as a (strict) sub-term.

But if you can think of a case that we should be testing for but aren't, I'll add a test to see if we can trigger some problem here.

[bugarela]

Ah, I see! So there is no such thing as cyclical bindings in our effect system anymore, right?

[shonfeder]

Not at the level of "entity" variables, because they can only stand for sets of state variables. But there might be something that can happy with effect variables. I haven't looked at that logic as part of this. Could be that we don't have rich enough structures to make that possible tho?

[bugarela]

Oh, right. At the effect level we have operators, so we should have cyclical bindings in things like e0 =.= (e0) => Read['x'].

Thanks for helping me get this context back in and understanding the scope of your solution!

[shonfeder]

Thanks for talking it thru with me and for the review! That is exactly right w/r/t effect variables. I think what we have here is just a special case due to simplicity of the "entity variables".

[bugarela]

Great finding! I've been scared of unification of sets since I first wrote this stuff, so I'm glad you were able to reason about this and implement proper binding.