IMO, requiring substitivity (forall a b. if a == b then forall f. f a == f b) is a pretty onerous condition for Eq as it is used in practice. Usually type class laws only govern how the type class methods interact with each other and with super classes. The substitutivity law places a requirement on the entire publicly exported interface for a type. The `Set` type in containers is in violation of this law as well (with `f = splitRoot`).
Laws are primarily sold to developers as a means of refactoring fearlessly - eg i can rewrite `fmap f . fmap g` into `fmap (f . g)` without altering the meaning of the given program. I'm not sure which refactors are possible with the substitutivity law.