Good question! The trick is that `match` is passed an (n-ary) Haskell function on embedded terms (in the example hidden as a lambda-case) which it can continually re-apply, forcing every case alternative to succeed in turn so that we can explore the right-hand-side of each equation. This is necessary because we have staged compilation; the Haskell case statement is being resolved at an earlier stage (and possibly on a different device) than when we find out which branch actually succeeds. I think it's an interesting use case for explicitly bi-directional pattern synonyms which I haven't seen before.