David S. Warren - 2013-09-03

The problem is your expectation of the meaning of the syntax of mod:foo(X). This is just a term, like any other. Functor symbols are in modules, so foo/1 can be in different modules, and in your case, by thinking carefully of how modules are assigned to functor symbols, we see that in one case the functor symbol foo/1 of m1:foo(X) is in m1, and in the other it is in usermod. So these two terms are not syntactically identically, and unification fails.

The syntax mod:foo(X) is treated in a particular way in certain predicates. Predicates that manage predicates (like call/n, assert, retract, ...) treat the syntax mod:foo(X) to mean foo(X) with foo/1 in module mod (regardless of what module f/1 in that term actually happens to be in.) So mod:foo(X) is treated specially by certain predicates that take predicates as arguments. If you want to compare whether two modified calls would actually be the same, you could write an explicit comparison predicate as:

same_call(Mod1:Goal1,Mod1:Goal2) :-
    Call1 = Call2.