<div dir="ltr">Thanks Henning, and apologies for the delay in replying.<div><br></div><div>I more had in mind your `n + 'Zero -> n` example. With cunning overlaps you can also achieve `'Zero + n -> n`; and even from result 'Zero improve both arguments to 'Zero.</div><div><br></div><div>With class ForthBack, a FunDep right-to-left would (maybe) expand  `a` to `Forth (Back a)` -- which hardly seems helpful and is anyway not true: `Forth (Forth (Back (Back a)))` would be just as legit.</div><div><br></div><div>That kind of recursion-depth-sensitive normalisation is possible with FunDeps and overlaps. But I'd need to recharge my Oleg batteries.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 23 Jan 2023 at 21:23, Henning Thielemann <<a href="mailto:lemming@henning-thielemann.de">lemming@henning-thielemann.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
On Mon, 23 Jan 2023, Anthony Clayden wrote:<br>
<br>
> > ... rewrite rules for type constraints ...<br>
<br>
> That's what FunDeps are, with the advantage you can stipulate <br>
> multiple/multi-directional rewrites.<br>
<br>
How would you simplify Forth (Back a) to 'a' automatically with FunDeps?<br>
<br>
I could define<br>
<br>
   class ForthBack a b | a -> b, b -> a where<br>
<br>
but then I would have constraint ForthBack a b and it does not go away.</blockquote></div>