Dear all, Last time around that we had a discussion about this proposal, the authors asked to have some more time to revise a few things. Since then, the proposal has been simplified, and the paper accepted (congratulations!). Last time around, those of us who opined were mostly in agreement with accepting the proposal, though there were some distracting complications. Which have since been forked (and accepted) as proposal #287 https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-si.... I do believe that this iteration of the proposal is a no-brainer. It simply gives a clear semantics to the unspecified -XImpredicativeTypes. It’s useful, and an implementation already exists (!3220 https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3220). The summary of the proposed specification is: to instantiate a type variable to something of the form forall a. …, go through arguments and look for an absolutely necessary such instantiation (which will happen when there is a data constructor: [a] ~ [forall b.t] iif a = forall b.t). The only point which we may want to discuss is ($), which currently has an ad hoc typing rule baked in the type checker. The proposal suggests removing this baked in rule, and replacing it with making ($) always use the -XImpredicativeTypes typing rule. An alternative, of course, is to simply not treat ($) any specially, and require -XImpredicativeTypes to be explicitly turned on when one wants runST $ do …. But, as the proposal points out, this would break a lot of existing programs. So I agree with the proposal’s choice. In summary, I recommend accepting this proposal in its current state.