Hello all, I recently noticed that GHC rejects the following program: type family F a b :: Constraint where F a a = () eq :: F a b => a :~: b eq = Refl This is certainly not shocking, but it is a little unsatisfying: as far as I can tell, accepting this program would be entirely sound. That is, `a ~ b` is morally a “superclass” of `F a b`. In this example the type family is admittedly rather pointless, as `a ~ b` could be used instead, but it is possible to construct more sophisticated examples that cannot be so straightforwardly expressed in other ways. I am therefore curious: has this kind of scenario ever been discussed before? If yes, is there a paper/GitLab issue/email thread somewhere that discusses it? And if no, is there any fundamental reason that GHC does not propagate such information (i.e. it’s incompatible with some aspect of the type system or constraint solver), or is it simply something that has not been explored? (Maybe you think the above program is horrible and *shouldn’t* be accepted even if it were possible, but that is a different question entirely. :)) Thanks, Alexis