Now that I've got the bit between my teeth ... Superclass constraints are not subject to the Paterson conditions. IOW I can write superclass constraints that are not permitted as instance constraints. (Superclass constraints are required to be non-cyclic, which ensures they're terminating.) Is that worth adding to the docos? Something like this is OK:

class (F a b ~ b) => C a b ... -- equivalently class (D a b b) => C a b ...

Can I think of a use for that? Maybe ... Sometimes even though you have a type function, you can use knowledge of the result to 'improve' the parameters. The classic case is adding type-level Naturals. Maybe even type-level Boolean And: - if the result is True, so must be the params. - if the result is False, and you know one param is True, the other must be False. - but that can't be a function, because if the result is False and you know one param is False, that tells nothing about the other param. AntC

...

On Sun Apr 30 19:45:34 UTC 2017, Richard Eisenberg wrote:

...

Documentation is just about always suboptimal -- but the best people to suggest concrete improvements are those who were confused to begin with. So, by all means, submit patches!

OK. Done. See #13657.