I just completed the cycle and realized my (second) stupid mistake. Realizing one stupid mistake and patching it makes it really hard to find more, I find: the little burst of satisfaction at patching the one seems to all but blind me to further faults. But I succeeded anyway. Gotta watch out for that sneaky eta-expansion. So the decidability of higher-order matching is still open; you can all sleep soundly now.
Hmm... what was the problem the last this happened? MELL provability decidability, I think.