I am implementing syntactic anti-unification for TH terms (Exp, Pat, Clause, ...). For example anti-unifying the clauses tail (1:xs) = xs tail (1:2:xs) = (2:xs) would yield tail (1:x1) = x1 whereas the anti-instance of last (1:[]) = 1 last (1:xs) = last xs is last (1:x1) = x2 So different subterms are always replaced with the same variable if anti-unified twice. So far, so good, there is nothing complicated. I am using a State Monad to keep track of my variables and defined a type class for anti-unification and implemented instances for Exp, Pat, ... type AU a = State (Data.Map [a] a) a class Antiunifieable t where antiunify :: (Ord t) => [t] -> t antiunify = (\t -> evalState (aunify t) M.empty) aunify :: (Ord t) => [t] -> AU t Problems arise when I come to clauses, defined in TH as Clause [Pat] Body [Dec] where Body is for example NormalB Exp Since a term can occur both as a pattern on the left-hand side of the equation and also as expression on the right-hand side, I need to keep track of this, too. So in fact, I have to anti-unify the patterns, 'translate' the resulting state (Data.Map [Pat] Pat) to (Data.Map [Body] Body) and pass it to the state transformer for anti-unifying the bodies. Similarly, from Body to Exp. This seems a bit ugly to me, but I have no idea how to solve it more elegantly. I thought about introducing some kind of wrapper type like data Term = TC Clause | TB Body | TP Pat | TE Exp and implement an instance for Eq and Antiunifieable for it. But again, this is not better either and I run into a lot of bookkeeping when processing it. Is there some kind of best practise dealing with such a problem? I am not sure if MonadTransformers would help here, because it is always the same monad but with different parameter. Thanks a lot, Martin