Afterwards I showed
Got dinner with
As I was walking home I thought of another angle for attacking type-safety of unification with forbidden-subterm placeholders. I say this every time, but I really think this one has the best chance yet of working — the particular reason is that it is vastly more syntactic than before, and keeps more information around in the terms themselves in a nice structural way.