[Haskell-cafe] syntactic anti-unification of TH terms --- best practise?

[Martin Hofmann]

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