In your class Sum example,

class Sum x y z | x y -> z, x z -> y

your own solution has a bunch of helper classes

First of all, on the top of other issues, I haven't actually shown an implementation in the message on Haskell'. I posed this as a general issue. In special cases like below > class Sum2 a b c | a b -> c, a c -> b > instance Sum2 Z b b > instance (Sum2 a' b c') => Sum2 (S a') b (S c') > -- note that in the FunDeps, var a is not a target > -- so the instances discriminate on var a I didn't doubt the translation would go through because there is a case analysis on a. But the general case can be more complex. For example, class Sum2 a b c | a b -> c, a c -> b instance Sum2 Z Z Z instance Sum2 O Z O instance Sum2 Z O O instance Sum2 O O Z

In your overlap example you introduce a definition that won't compile!

...

{- -- correctly prohibited! instance x ~ Bool => C1 [Char] x where foo = const True -}

You expect too much if you think a mechanical translation will 'magic' a non-compiling program into something that will compile.

I do expect equality constraints to not play well with overlaps. Combining FunDeps with overlaps is also hazardous. I'm only claiming that EC's will be at least as good.

I don't understand the remark. The code marked `correctly prohibited' is in the comments. There are no claims were made about that code. If you found that comment disturbing, please delete it. It won't affect the the example: the types were improved in t11 but were not improved in t21. Therefore, EC's are not just as good. Functional dependencies seem to do better.