An example, which is obscure too, but cannot be de-obscured in same way as you have done above, is:

Code: Select all

open core
class predicates
test : (unsigned X).
clauses
test(X) :-
tuple(A, X) = tuple(B, B), % throws errors: Variables "A", "B" are not completely bound
stdIO::write(A, ", ", B).
clauses
run() :-
test(1).

Both

**A** and

**B** are free initially, thus it cannot be re-written as:

Code: Select all

open core
class predicates
test : (unsigned X).
clauses
test(X) :-
A = B, % illegal
X = B,
stdIO::write(A, ", ", B).
clauses
run() :-
test(1).

Of course it is easy to see that it can be de-obscured in another way:

Code: Select all

open core
class predicates
test : (unsigned X).
clauses
test(X) :-
X = B,
A = B,
stdIO::write(A, ", ", B).
clauses
run() :-
test(1).

But that other way is obvious only because the example is very small. We could pump the code up by using many variables and algebraic expressions instead of only

**A** and

**B**, so that we obtain a complicated example, for which it is by no means easy to figure out, how to de-obscure it.

Hence de-obscuring an obscure unification means, that the programmer is performing a substantial part of the unification-computation in advance. However we have the expectation that the system does all the unification-computation by itself.