programming - Why does Mathematica choose the second function definition?

While working on a solution to this question I've come across a case where I simply don't understand Mathematica's behaviour.

I've got the following definitions:

PatternImplies[(x:(Verbatim[Blank]

                  |Verbatim[BlankSequence]
                  |Verbatim[BlankNullSequence]))[h_],x[]]:=True

(*CatchAll rule*)
PatternImplies[_,_]:=Maybe;

Now I try this:

PatternImplies[_Integer,_]
(*
==> Maybe

*)

I would have expected True. My first thought was that I probably got the pattern wrong, so I tested:

MatchQ[PatternImplies[_Integer,_],
       PatternImplies[(x:(Verbatim[Blank]
                         |Verbatim[BlankSequence]
                         |Verbatim[BlankNullSequence]))[h_],x[]]]
(*
==> True
*)

In other words, the pattern matches. Moreover, looking at Downvalues I see that the special rule is indeed stored before the catch-all rule.

So why does Mathematica chose the second definition (and more importantly, what can I do about it?)

Answer

As far as I can tell, it should match the catch all rule. That's because _ isn't of the form x[]

Now, when you test the MatchQ expression, both arguments are first evaluated. So, you're actually doing MatchQ[maybe, maybe] which of course returns True.

You can do the checking as you intended to by first holding the arguments

MatchQ[Hold@PatternImplies[_Integer, _], 
 Hold@PatternImplies[(x : (Verbatim[Blank] | Verbatim[BlankSequence] |
         Verbatim[BlankNullSequence]))[h_], x[]]]


False

EDIT:

I now see what you intended with x[]. You could do x_[] instead. That would mean "any no-argument expression whose head coincides with the previous pattern labelled x. If you write x[] it matches literally