Hi, there might be a bug that looks to be related to variable instantiation.
To see it, run: ?- freeze(Ns, sum(Ns, #=, 2)), append([1], [1], Ns).
You get: ERROR: Arguments are not sufficiently instantiated
A workaround is: ?- freeze(Ns, sum(Ns, #=, 2)), append([1],[1], Vs), Ns = Vs.
It works as expected (but doesn’t look elegant).
Any thoughts and comments? Thanks in advance!
The signature of sum/3 is sum(+Vars, +Rel, ?Expr), which informally should be read as Vars must be instantiated to a list. As the first iteration of append/3 binds the 3th argument to a partial list, freeze/2 triggers sum/3 too early.
Constraints relax ordering problems, but does not fully remove them … Of course, this could be fixed inside sum/3, after which you no longer need freeze/2.
Thanks Jan! This makes sense.
But could you elaborate a bit why append/3 has to bind the 3rd argument to a partial list instead of a list ?
In other words, could this be fixed in append/3 (also append/2), or are there good reasons to keep it as a partial list ?
The third argument becomes a proper list eventually. But freeze/2 fires as soon as its first argument is not a free variable. At this point the list looks like [1|_], which is indeed a partial list. This should be visible in the full error message you get.
If you used when(ground) instead of freeze:
?- when(ground(Ns), sum(Ns, #=, 2)), append([1], [1], Ns).
Ns = [1, 1].
It doesn’t have to. It does, because it’s quick and usually acceptable.
Could use instead:
copy_list_tail([], Tail, Tail).
copy_list_tail([H|T], [H|T2], Tail) :-
copy_list_tail(T, T2, Tail).
append_two_lists(L1, L2, Both) :-
copy_list_tail(L1, BothN, L2),
% Finally, unify Both
Both = BothN.
… which will work as desired, because it doesn’t instantiate Both until the end:
?- freeze(Ns, sum(Ns, #=, 2)), append_two_lists([1], [1], Ns).
Ns = [1, 1].
This is a special-purpose predicate, due to the deliberately-delayed unification, which is against the fail-fast principle, because Both can only be compared at the end.
Thanks Boris!
Using when(ground(Ns), …) solves this example problem. However in my actual project ground(Ns) is too strong and I do need freeze to allow Ns to be a list of FD variables constrained by sum/3.
Thanks Brebs,
Yes, this solution is similar to my workaround suggested in the initial question. It does work, but just feeling append/3 should address it internally.
I’d recommend to not mix freeze with clp. Why use freeze?
An alternative to freeze/2 is when(nonvar), but the error remains the same.
This is a specialized use-case. append/3 should not be weakened in its fail-fast property, just for this use-case. Can use custom code instead of append/3 
Yeah, makes sense! So I actually did that 
Good to learn some internal working of Prolog though.
Thanks Brebs!
Do you really need to use freeze? Perhaps your code could be written to be nicer and faster without freeze 