Counterintuitive DownValue precedence

Question

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.

(emphasis mine)

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 True)

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

Answer 1

Mathematica does try to move more specific downvalues in front of less specific downvalues. You should note that the most specific possible downvalue is one which does not include any patterns (e.g., Blank, Condition, etc). These kinds of downvalues are called literal downvalues, and they are always ordered first, because Mathematica can use hashing to optimize these downvalues. So, taking your first example:

Clear[foo]

foo[a] /; True := b
foo[a] := a

DownValues[foo]

{HoldPattern[foo[a]] :> a, HoldPattern[foo[a] /; True] :> b}

Here the literal downvalue foo[a] will always come first. For your second example:

Clear[foo2]

foo2[a_] /; True := b
foo2[a_] := a

DownValues[foo2]

{HoldPattern[foo2[a_] /; True] :> b, HoldPattern[foo2[a_]] :> a}

In this example, both downvalues are patterns, and since Mathematica is able to determine which downvalue is more specific, it will reorder the more specific downvalue in front of the less specific downvalue.