Hi, here's is the problem I was talking about yesterday in a distilled form:

I want to talk about datatypes which have deep recursive structure, ideally:

class (WellFormed a, All2 WellFormedR (Code a)) => WellFormedR a where

This would work, with some extensions like UndecidableSuperClasses, if I could
instantiate leaf types, like Int, with something like:

instance All2 WellFormedR (Code Int) where

This cannot happen because All2 is a type synonym and cannot be directly
instantiated, and `Code Int` does not really evaluate to an actual list of list
of types.

Now, there are libraries which deal with this recursive idea (see the recent
generics-mrsop) but they bring a lot of problems that imho are unnecessary in
this use case, because I actually don't care for the recursive position of the
same datatype (ie. in Foo, I don't care to know the recursive positions in which
I have Foo - I just want to treat uniformly the recursion).

The motivation for this kind of structure this time is that I want to talk about
typed substitutions for a prolog-like engine, I have working code here [0], and
I was progressing smoothly with a few workarounds until I had to write a type
signature for:

unify :: (?) => Term a -> Term a -> Unification Substitution

As the subterms have to be unified, they have to share the same constraint I
put on unify, recursively, and I haven't found a workaround for this.

If you have any ideas on how I should approach this problem and why, please
share!

[0] https://gist.github.com/meditans/a0d3075c3a6f99f73c598c5bd839b2b3