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
PmGrds into constraints that the oracle understands.