This may be considered an implementation detail and not a guaranteed behavior. The underlying set theory is predicated on a notion of an equivalences classes rather than on object identity. The implementation takes full advantage of that fact in its operations. For example, set intersection makes an implementation dependent choice for which of two equivalent zeros to return:

>>> {0, 1}.intersection({0.0})
{0.0}
>>> {0.0, 1}.intersection({0})
{0}
>>> {0}.intersection({0.0, 1})
{0}
>>> {0.0}.intersection({0, 1})
{0.0}

I think the situation is similar for dicts where d[k] = v for an existing key guarantees that k keeps its insertion order and that v is always replaced, but no assurance is given about whether k is replaced. Python currently does not replace k but a case could be made that perhaps it should be replaced so that the final k and v correspond:

>>> d = {0: 1}     # The types match:  int -> int
>>> d[0.0] = 1.0.  # The types match:  float -> float
>>> d              # The types no longer match:  int -> float
{0: 1.0}

I would support a note that the behaviour is implementation-defined, not specified by the language, and users should not make any assumptions about which element is kept.

Given that CPython is the reference implementation, I think that it is fair to document which parts of the behaviour are not considered part of the language and so (1) do not need to be emulated by other implementations and (2) should not be relied on.