Especially when I expect them to!
Yes, so discovered what the bug was in the middle of it. Things were falling into a default case in weak head-normalization when they shouldn't have. Very strange! It's things like these that make me upset that some ML hackers don't mind letting non-exhaustive matches remain in their programs, because the notion of not covering all the cases the way you expect seems to be such a common source of errors for me. Sadly, even if the makers of twelf had programmed with such discipline, it wouldn't have helped me find this particular bug, because there was a fall-through case that caught the new possiblity, (making the match indeed exhaustive, even though I would never notice one more non-exhaustive match warning in the huge swaths of them) and did the wrong thing with it. I wonder how one might help the compiler alert the programmer to such subtle dangers.