Ah, I thought your username was familiar: you recommended Wadler's approach on a previous HN thread concerning my blog post about Pettersson/Maranget's algorithm (https://news.ycombinator.com/item?id=39241776). Yeah, I admit that Pettersson's telling of the algorithm is a bit turgid (probably why Maranget's paper - which is the same technique as its core, at least to my understanding - is cited more often).