UWN

I read your sentence "The issue is more readily observed with a custom propagator" as implying that you have a direct `clpz` program (without any propagator) that still exposes this...

SWI tried this. And [so far failed](https://github.com/SWI-Prolog/issues/issues?q=is%3Aissue+dif%2F2). This is extremely complex for minor gains. Definitely a work sink. And, it is already non-trivial for terms, even worse for rational trees...

@infradig: An even more unreadable case in SWI is #2029

Also note that the [documentation incorrectly states](https://ciao-lang.org/ciao/build/doc/ciao.html/terms_check.html#subsumes_term/2) that Ciao checks for an instance. However, ``` ?- subsumes_term(f(X,X),f(Y,X)). yes, unexpected. % this is not even an instance ?- subsumes_term(f(Y,X),f(X,X)). yes %...

Currently, the following twelve implementations implement this correctly: B, ECLiPSe, GNU, Ichiban, SICStus, SWI, Scryer, Tau, Trealla, X, XSB, YAP.

Also note that the [documentation](https://ciao-lang.org/ciao/build/doc/ciao.html/terms_check.html#subsumes_term/2) neither agrees with [Cor.2](https://www.complang.tuwien.ac.at/ulrich/iso-prolog/dtc2#subsumes_term) nor does it agree with the current implementation, as it incorrectly reads: > `subsumes_term(Term1,Term2)` [ISO] > `Term2` is an instance of...

A shorter example: ``` ?- subsumes_term(f(X,X),f(_,X)). yes, unexpected