I find it a bit hard to justify this change, which might thus fall until the principle of "if it ain't broke, don't fix it": is there any chance that we would change this implementation in the future? I suppose that you propose this because you are yourself interested in adding new fields, could you talk a bit more about what your use-case is? Is this a change that you already performed in one of the copies/variants/ports of the implementation that exist in the wild, and that you are only backporting to the standard library?

I don't understand. Your principle "if it ain't broke, don't fix it" implies that there is a potential risk/cost associated with a change.

I don't see any risk/cost here. The changes are simple and the map module should be well tested.

It makes the code a bit cleaner and closer to modern idioms without a downside. Isn't that enough ?

What is the aim/gain of this change ? The rationale "should make it easier to add fields to ... in the future" can potentially apply to every single tuple type definition ... I doubt anyone would advocate to change every tuple by a record, right ?

there is a valid use case for people to copy paste code though
For example, user may want to book keep size of the set for his own map/set, 2 cents

is there any chance that we would change this implementation in the future?

Probably not.

I suppose that you propose this because you are yourself interested in adding new fields, could you talk a bit more about what your use-case is?

I want to know how my maps are used, number of backtrack, number of Not_found, age of nodes.
I also want to know if the nodes that i add between each of my backtrack are used.

What is the aim/gain of this change ? The rationale "should make it easier to add fields to ... in the future" can potentially apply to every single tuple type definition ... I doubt anyone would advocate to change every tuple by a record, right ?

Obviously not, but if someone propose to make this job for the community why can't we accept it ?

We discussed this at the developer meeting two days ago and some of us were a bit dubious because this doesn't change anything for users. In the end, we decided to merge it because it improve the quality of our source code, and this is worth the (small amount of) trouble.