I'm generally positive on the goal of figuring out better record support in GHC.
That said, it isn't clear that Nikita's work here directly gives rise to how the syntax of such a thing would work in GHC proper. Simon's original proposal overloaded (.) in yet more ways that collide with the uses in lens and really drastically contribute to confusion in the language we have. This is why over the summer of 2013 Adam Gundry's proposal evolved away from that design. Nikita on the other hand gets away with using foo.bar syntax in a more lens-like fashion precisely because he has a quasi-quoter isolating it from the rest of the language.
If you strip away that layer, it isn't clear what syntactic mechanism can be used to convey the distinction that isn't taken or just as obtrusive as the quasi-quoter.
But, "it isn't clear" is just code for "hey this makes me nervous", so let's spitball a couple ideas:
Nikita's proposal has two things that need addressing:
1.) The syntax for record types themselves
2.) The syntax for how to get a lens for a field
Re #1
The main term and type level bits of syntax that could be coopted that aren't already in use are @ and (~ at the term level) and things like banana brackets (| ... |), while that already has some other, unrelated, connotations for folks, something related like {| ... |}. We use such bananas for our row types in Ermine to good effect.
The latter {| ... |} might serve as a solid syntax suggestion for the anonymous row type syntax.
Re #2
That leaves the means for how to talk about a lens for a given field open. Under Adam's proposal that had evolved into making a really complicated instance that we could extract a lens from. This had the benefit over the current state of the `record` package that we could support full type changing lenses. Losing type-changing assignment would be a big step back from the previous proposal / the current state of development for folks who just use makeClassy or custom lens production rules with lens to get something similar, though.
But the thing we never found was a nice short syntax for talking about the lens you get from a given field (or possibly chain of fields); Gundry's solution was 90% library and almost no syntax. On the other hand Adam was shackled by having to let the accessor be used as a normal function as well as a lens. Nikita's records don't have that problem.
Having no syntax at all for extracting the lens from a field accessor, but rather to having it just be the lens, could directly address that concern. This raises some questions about scope, where do these names live? What happens when you have a module A that defines a record with a field, and a module B that does the same for a different record, and a module C that imports both, but, really, we had those before with Adam's proposal, so there is nothing new there.
And for what it is worth, I've seen users in the wild using makeLenses on records with several hundred fields (!!), so we'd need to figure out something that doesn't cap a record at 24 fields. This feedback came in because we made the lenses lazier and it caused some folks a great deal of pain in terms of time spent in code gen!
It is a long trek from "this is plausible" to "hey, let's bet the future of records and bunch of syntax in the language on this".
It would also necessarily entail moving a middling-sized chunk of lens into base so that you can actually do something with these accessors. I've been trying to draw lines around a "lens-core" for multiple years now. Everyone has a different belief of what it should be, and trust me, I've heard, and had to shoot down basically all of the pitches.
We're going to be stuck with the warts of whatever solution we build for a very long time.
So with those caveats in mind, I'd encourage us to take our time rather than rush into trying to get this 7.12 ready.
Personally I would be happy if by the time we ship 7.12 we had a plan for how we could proceed, that we could then judge on its merits.
-Edward