dif/2 incorrect Ⅴ

[UWN]

?-            A=[[]|A], B=[C|D], D=[_|_], D=[[]|C], dif(A, B).
A = [[]|A],
B = [C, []|C],
D = [[]|C].

?- dif(A, B), A=[[]|A], B=[C|D], D=[_|_], D=[[]|C].
false, unexpected.

?-            A=[[]|A], B=[C|D], D=[_|_], dif(A,B), D=[[]|C].
false, unexpected.

(version 9.1.4)

[UWN]

?-            A=[[]|A], B=[C|D], D=[_|_], dif(A,B), D =[F|C].
A = [[]|A],
B = [C, F|C],
D = [F|C].

?-            A=[[]|A], B=[C|D], D=[_|_], dif(A,B), D =[F|C], var(F), copy_term(F,FC,G_0s).
A = [[]|A],
B = [C, F|C],
D = [F|C],
G_0s = [].

?-            A=[[]|A], B=[C|D], D=[_|_], dif(A,B), D =[F|C], var(F), copy_term(F,FC,G_0s), F = [].
false, unexpected.

How is it possible that unifying an uninstantiated, apparently unconstrained variable leads to failure?

[UWN]

Same problem with finite terms:

?- A=[[]|C], B=[D|A], C = [_|_], dif(A,B), C=[E|D], E = [].
false, unexpected.

OK with set_prolog_flag(occurs_check, true)., unexpected error with set_prolog_flag(occurs_check, error). (but indeed same error when dif(A,B) is replaced by A \= B)

[JanWielemaker]

Last one now works with SWI-Prolog/swipl-devel@ea776fdcc7bbc255b2ae882cd81b79de7c34d254. The whole thing is too complicated and needs detailed comment and possibly redesign :cry:

[JanWielemaker]

This issue has been mentioned on SWI-Prolog. There might be relevant details there:

https://swi-prolog.discourse.group/t/cleanup-dif-2/6274/1

[UWN]

113 is probably the more fundamental one. After all, if there is non-termination chances to find terminating counterexamples diminishes.