Finally, there are Sections 6 to 8. These are entirely new. Though they are working towards the new principles (well, as far as I can tell, Section 6 doesn't contribute to the principles, but it is a stepping stone for both Sections 7 and 8). These sections are concerned with adding local let-bindings of type variables, in particular inside types and patterns.
By the way, Section 7 proposes two syntaxes for let binders in patterns, and I *strongly* prefer the second syntax, which reads something like `f (let b = Bool) (True :: Bool) = …`.
Anyway, these are new, I feel that they are a bit out of place in a proposal that is about tidying up the existing designs. That being said, they are here, and they seem like fairly uncontroversial to me, (except, probably the syntax `(let b = _)` to bind a variable to a type to be filled by the compiler). I'm fine with accepting these, though they may require a bit more scrutiny than the rest.
Best,
Arnaud