Functional dependencies and type families

Consider

type family F a :: *

class C a b | a -> b

instance C p (F q) => C p [q]

Is the instance decl OK under the liberal coverage condition?

That is, does (C t [s1], C t [s2]) mean that (s1 ~ s2)?

NO! The context of the instance declaration means that p -> F q but that does not imply p -> q unless F is injective!

So this program is wrongly accepted.

I realised this when investigating #10778.