I'm feeling conflicted about theory.pod. While I'm very proud of it for being a great object model and giving precise semantics to things we've been handwaving over for ages, it just isn't Perl. It's too formal and static for Perl; you can't talk it into checking something a different way.
However, it is not possible to add a pure hook system that's reasonable for the everyday user to use. Type inference can't deal with arbitrary code, because it needs to go forwards and backwards and sideways through the annotations to figure things out, whereas arbitrary code can only go forwards. If we had a logic subsystem, we could give them arbitrary code (within that subsystem) because logic programming has the nice property that you can execute a function backwards:
:- append(X, Y, [1,2,3,4,5]).
But maybe instead I need a coproposal, one that really gets down and dirty with Perl 6's internals, for the hook system on top of which theory.pod can be built as a module. If that exists (assuming it is even possible), then I wouldn't feel so uneasy about theories not being arbitrarily flexible.