Exceeding recursion limit with no obvious recursion: Optional pattern-matching causing nonlocal behavior

So, I’ve come across something strange, and wanted to get a deeper understanding of what was going on. Consider the following code:

f[a : {{__}..}, k_ : 0] := 1

a = Table[Table[0, {5}], {10000}]

f[a, 2]

So, f takes a list of lists and a single optional expression, which can take the default value 0. This should obviously give 1, right? After all, the arguments seem ok: MatchQ[a, {{__}..}] gives True, and even MatchQ[{a, 2}, {{{__}..}, _}] gives True. More closely, even,

MatchQ[{a, 2}, {{{__}..}, _ | PatternSequence[] }]

gives True.

However, instead of producing 1, f[a, 2] gives an error message "General::maxrec: Recursion limit exceeded; positive match might be missed." and does not evaluate further.

This behavior is also present when defining Default[f]. And, indeed, as soon as we use the Optional pattern in MatchQ[{a,2}, {{__}..}, k_:0}], MatchQ breaks down and gives the same error message as f does. But it can be avoided by removing the default value and providing it in a different (but still definitional) way, e.g.

(* Works: *)

f1[a : {{__}..}] := f1[a : {{__}..}, 0]

f1[a : {{__}..}, k_] := 1

(Also, it doesn’t happen with the shallower pattern a : {__}.)

Now, I’m not the first person to notice this behavior and ask about it here. The answer there says it was an intentional change, and I understand there were probably good reasons—I’m not asking for the rationale, or how to change it. But this is not a duplicate question (at least not to that one), because I’m trying to figure something that wasn’t asked there:

---

Why does the Optional pattern, e.g. k_:0, put a recursion limit on matching the pattern occurring before it? Why does it do so when apparently equivalent pattern matchings (such as k:(_ | PatternSequence[]), the alternative implementation of a default value for f, or a match made in isolation) don’t?

---

Note: A previous version of this question asked why the behavior of pattern matching for function definitions didn’t agree with the behavior of pattern matching for MatchQ, until @WReach pointed out in the comments that they do, in fact, agree! I simply wasn’t using the same pattern verbatim to check.

Possibly related question: the linked answer says something about "dynamic backtracking"; what is that, and is that somehow present for Optional matching but not the other working matchings shown here?