Conversion of distributive type families of constraints

Question

Hypothesis: Type families which result in Constraints are always distributive over their representational parameters.

As an example, Fam x Eq `And` Fam x Show is equivalent to Fam x (Eq `And` Show) if Fam's second parameter has a representational role.

Questions:

• Is the above hypothesis indeed correct? Are there any references to it?
• Does GHC somehow allow utilising this rule to convert equivalent constraints?

Answer 1

Intuitively, this breaks down if Fam x c uses c in a contraviariant way. This is now possible using quantified constraints. E.g.

Fam x c = (forall a. c a => D a x)

for some D a x :: Constraint.

(I think this is representational, even if I'm not completely positive.)

Hence Fam x (Show `And` Eq) would mean

forall a. (Show a, Eq a) => D a x

while (Fam x Eq, Fam x Show) would mean

( forall a. (Show a) => D a x
, forall a. (Eq a) => D a x )

The two constraints are not equivalent. For instance, if D a x = (Show a, Eq a) the former is trivially satisfied, while the latter is not.