Consider the following definitions for two symbols:
foo[a] /; True := b foo[a] := a foo[a] (* a *) foo2[a_] /; True := b foo2[a_] := a foo2[a] (* b *)
(The order of the definitions does not matter in both cases)
This documentation page says:
When you make a sequence of definitions in the Wolfram System, some may be more general than others. The Wolfram System follows the principle of trying to put more general definitions after more specific ones. This means that special cases of rules are typically tried before more general cases.
Although in many practical cases, the Wolfram System can recognize when one rule is more general than another, you should realize that this is not always possible. For example, if two rules both contain complicated /; conditions, it may not be possible to work out which is more general, and, in fact, there may not be a definite ordering. Whenever the appropriate ordering is not clear, the Wolfram System stores rules in the order you give them.
Reading this, it is clear that we are not in the case where the system can't decide (as order is irrelevant), but rather in the case where it "knows" which rule is more specific. The question is now:
Why would the rule
foo[a]:=... be more specific than
foo[a]/;True:=...? It seems pretty obvious that this is not the case... (especially if the condition is not simply
Note: This is not a duplicate of this question - I'm asking about the possible reasoning behind a specific case, not the general algorithm at work