Pattern variables should be lifted to top level

...since pattern variables scope across the whole expression. If we
don't lift them, mysterious unification errors can happen for implicit
arguments.