I think I found a relatively sane solution to the expression problem, which employs quite a weird type system. The trick is to use a permissive (nearly "dynamic") first typing pass, using a "weak set" unification (a special kind of a Prolog variable which unifies with any other weak set, merging the values together), and then doing another typing pass to find out of the union types inferred this way are isomorphic to the expected declarations.

This way, tagged unions can be expanded, cut down, rewritten using simple rules - all the stuff you can do in Nanopass, but strictly typed with a Hindley-Milner type inference.