Simon realised that the simple language composed of let bindings, bang patterns and flat constructor patterns is enough to capture the semantics of the source pattern language that are important for pattern-match checking. Well, given that the Oracle is smart enough to connect the dots in this less informationally dense form, which it is now.
So we transform translatePat to return a list of PmGrds relative to
an incoming match variable. pmCheck then trivially translates each of
the PmGrds into constraints that the oracle understands.