Unification fails to substitute via most specific unifier when variables are bound to variables

[ngeiswei]

What is the problem?

Unification such as (A $a $a) ≐ (A $x $y) fails to recognize that $x = $y.

How to reproduce the problem?

Run the following metta code

(A $a $a)
!(match &self (A $x $y) (A $x $y))

What should be normally output?

It should output (A $x $x) or (A $y $y) (or even (A $a $a) if the variables present in the query are not prioritized).

What is output instead?

(A $x $y)

What else can you tell?

When variable $a is replaced by a, as in

(A a a)
!(match &self (A $x $y) (A $x $y))

it outputs the correct answer (A a a), so the problem really has to do with bindings between variables.

[ngeiswei]

That issue could be related to #516, potentially.

[vsbogd]

Unification inside grounded MatchOp implementation works correctly, but bindings like { $x = $y } are incorrectly applied to the pattern. There are two possible ways to solve this issue:

1. application could rename variables of the template to make them equal
2. we could return bindings with the result.

Option (2) is not allowed by current GroundedAtom API. It is implementable and I even evaluated this approach. But I didn't raise a PR because I thought that allowing this will make API more complex and users will be confused. I believe if we implement it then we need to keep ability to return results without changing bindings which is enough to the most of grounded functions. Thus allowing users to change bindings when it is required and don't touch them when it is not required.

So, I will try to fix it by renaming variables (option (1)).