This ticket tracks the task of removing implicit quantification in type synonyms, including the removal of the `-Wimplicit-rhs-quantification` warning flag. The flag was introduced in GHC 9.8 and added to `-Wcompat`, as per [GHC proposal #425](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst#scope). The proposal included the intention to remove it after three releases (so GHC 9.14). I would like to know what our plan is. As per the proposal, we can remove this mechanism and warning flag in 9.14. However, given that it was only part of `-Wcompat`, I think it might be nice to extend an additional courtesy to users. So I instead propose the following: 1. Enable the warning by default starting in GHC 9.14, and change the error message to indicate it will turn into an error in the next release. 2. Remove the implicit quantification mechanism in GHC 9.16. What do others think? Is the existence of this implicit quantification mechanism blocking anyone, or is it OK to delay its removal by one more GHC release? @int-index @sand-witch @simonpj