Generate a given quantified constraint?

[gelisam]

According to this note, it's possible for a plugin to generate new given constraints. Can we simply add quantified constraints like forall xs ys zs. ((xs ++ ys) ++ zs) ~ (xs ++ (ys ++ zs)) and then let ghc figure out whether it needs to apply them and avoid cycles? If that works, that would make using this library much safer, would make the implementation a lot simpler, and would probably support tricky wanted/given cases like in #3 !

[gelisam]

Manually adding such a quantified constraint is illegal:

-- Illegal type synonym family application ‘ys ++ '[]’ in
-- instance ((ys ++ '[]) ~ ys) in the quantified constraint
-- ‘forall (ys :: [*]). (ys ++ '[]) ~ ys’
foo :: (forall ys. (ys ++ '[]) ~ ys)
    => ((xs ++ '[]) ~ xs => r)
    -> r
foo r = r

So adding it automatically will be illegal too. Closing.