<div dir="ltr"><div>Dear all,</div><div><br></div><div>As the title implies: I'm hereby recommending accepting the Quick look impredicativity proposal.</div><div><br></div><div>Summary:</div><div><br></div><div>The proposal modifies the `-XImpredicativeTypes` extension with a well defined semantics which consists in considering n-ary applications, rather than binary. And look, in such an application, for arguments which absolutely require impredicative instantiation (either universally quantified type applications, or arguments where a universal type is guarded by an invariant type constructor).</div><div><br></div><div>In order to have the expected behaviour for `($)` and `(.)`, the proposal also makes the left-hand argument of the arrow invariant with respect to instantiation (currently: contravariant). The proposal is to make this change effective, even if `-XRankNTypes` is turned on, but not `-XImpredicativeTypes`. The proposal also introduces an extension `-XContravariantFunctions` to restore the old behaviour, for compatibility.</div><div><br></div><div>Rational:</div><div><br></div><div>`-XImpredicativeTypes` is a useful extension which is currently in a rather sad state. I'm happy to see it stabilise to a clear semantics. The semantics in the proposal covers a ton of use cases. It strikes a very good balance between usefulness and predictability.</div><div><br></div><div>The use of n-ary application in the type system also has good theoretical roots: sequent calculi have n-ary applications. (in manyrespects, bidirectional type systems are also about n-ary application). So I don't consider it a wart at all.</div><div><br></div><div>The propsal's semantics, including the absence of contravariant functions, goes in the direction of _guessing less things_. This is a direction that many GHC features have taken lately. I think it's a very very good direction! Guessing can be damaging for predictability, but. more importantly, guessing has a tendency to compose badly with other typing features. (it is to be noted, too, that the implementation of contravariant functions. in GHC, eta-expands the function, which can casually change its semantics, if the function was bottom).</div><div><br></div><div>So, everything in this proposal does look good to me, except that, I think, I would like a deprecation route for the `-XContravariantFunctions` extension. Otherwise, we will be stuck with legacy code forever.</div><div><br></div><div>Best,</div><div>Arnaud<br></div></div>