Signed-off-by: Edward Z. Yang <firstname.lastname@example.org>
Representational injectivity on type families says that if T a ~R T b, then a ~N b (N because type families are always nominal, at the moment.) This suggested that the following code might type check:
type family F a = result | result -> a f :: Coercible (F a) (F b) => a -> b f x = x
But in fact injective type families are never used for decomposition (i.e., replace this with F a ~ F b, it still won't type check), see https://ghc.haskell.org/trac/ghc/ticket/10833 so this seems to be a moot point.