Fix constraint eq

[clyben]

This PR fix #143 by adding a transformation on rules that substitute all x to y in both head and body when meeting (= x y) in the body. For example, (rule ((= x 1) (= y x) (= z y)) ((set (f z) 1)) is transferred to (rule ((= x 1) (= x x) (= z x)) ((set (f z) 1)) and then (rule ((= x 1) (= x x) (= x x)) ((set (f x) 1)). It also adds a new Type error similar to LocalAlreadyBound but with less information to deal with letting binding conflict in transformation.

After solving #143, PR #146 for seminaive should be able to go.

[oflatt]

This is a great fix @clyben
Unfortunately, I also fixed this bug in the PR I'm working on #158
I also did it as part of the existing desugaring functions, instead of as another pass on top of the desugared code.

I would recommend closing this PR for now, I'm hoping to get mine in soon.

[yihozhang]

Yeah this issue has to be fixed again in the new term encoding anyway. The issue itself is a bit tricky though-- Kevin and I had several back and forth before getting it right. So maybe let's keep this PR open until we can verify the merged term encoding does not have this issue (and have all the tests here ported)?

[clyben]

Could you add tests/constraint-eq.egg in my PR to your fork?

[oflatt]

Yep!

[oflatt]

Added to my PR and fixed! Thanks for great tests!

[mwillsey]

So this should be closed, since the fixes are coming in another branch?

[oflatt]

Fixed by #158

[clyben]

ok I will close it.

[yihozhang]

@clyben Could you re-open this issue since #158 is not going to be merged in the near future?

[oflatt]

As far as I know this was fixed by #176
let me know if that was not the case

[yihozhang]

Ah great, I didn't know that! The test from this PR seems to be passing in main, so I suggest closing this PR (again) and I'll make another PR porting the tests from this one.

@oflatt: It seems your #176 also subsumes #146, which was originally blocked by this PR. I will check if this is the case, and if so, we can close #146 as well.

[oflatt]

I think I also added the tests in this one to #176 but double check