It seems there are bugs with unification when a term has a variable used several times, but that variable isn’t used afterwards. The root cause seems to be in the definition of the
would_unify function of the Å-machine specification, but happens with z-code as well. A minimal example is as follows:
(test $A) ($A = [0 1]) (program entry point) (test [$X $X]) Unification is possible. (line) (test [$Y $Y]) Value of Y: $Y.
Here, “Unification is possible.” is printed, but the value of $Y isn’t. Besides, if we do not move the unification to its own rule but instead write this:
(program entry point) ([$X $X] = [0 1]) Value of X: $X.
Here we get “Value of X: 0.” which is printed, so unification seems to be incorrectly simplified by the compiler in this case.
Also, thanks a lot Linus for your work, Dialog is really awesome!