I think I have a fundamental misunderstanding about unification. Here are my two clauses:
test(func(X), X, 1) :- X == X.
test(func(X), Y, 0) :- X \== Y.
So- If I query test(func(X), Y, D), I would expect it to only be provable with the second clause, and D will be 0. This is because (I think\I am trying to) ensure that X must be equal to X, in the first clause. So my query shouldn't unify because X is not the same as Y. I thought == tests that the two operands are the same variables. And X and Y clearly aren't.
But the output:
| ?- test(func(X), Y, D).
D = 1
Y = X ? ;
D = 0
So it is saying that it unifies with the first clause if Y = X. But, Y is not equal to X. What am I misunderstanding here?
Your first answer, D = 1, Y = X accords with your first definition. I think you're expecting that when you query ?- test(func(X), Y, D). it should fail for the first definition, because the X and Y are different variables, but the first definition should only succeed if the two variables are identical.
However, in the head of your clause, you have the same variable appearing twice: test(func(X), X, 1) :- X == X. (As @CapelliC pointed out, X == X is superfluous here.) When you query ?- func(func(X), Y, D)., Prolog tries to unify this clause with the head of your first rule. It unifies func(X) with func(X) and Y with X and 1 with 1. Once this pattern-matching unification has succeeded, it then tests the body of the rule to see if the criteria are met. Since Y has been unified with X, the two variables will match the strict equality condition---during the pattern matching, you've unified Y with the same variable as X.
Note the following two queries:
?- X == Y.
false.
?- Y = X, X == Y.
X = Y.
The second is similar to what's happening with the query that's confusing you. If you rewrite your first rule in accordance with @CapelliC's suggestion,
test(func(X), Y, 1) :- X == Y.
Then it will function as expected, because, in this case, a free variable in the second argument will be unified with a different variable than that within the func/1 term, and then the two variables won't satisfy strict equality (but if the two variables are unified with a ground term, they will pass).