I want to think more about this and continue the conversation, but I'm worried the reply window will close first.
Since I presume your input space is relatively small (the AST of a program, which usually only has a few thousand nodes), it sounds like you have some sort of state-space explosion.
Your comment about recursive matching of hypertees sounds like the biggest problem.
Just a shot in the dark (having not studied what you're doing yet), but is there any chance you could use partial-order reduction, memoization, backtracking, etc. to reduce the state-space explosion?
I could be wrong, but most of the other optimizations sounded like they address constant factors, like contract checking.
But then I don't know much about how contracts work; I guess the verification logic could be rather involved itself.
If the window closes, maybe we could continue at #arc-language:matrix.org