`native.rb_map.insert` not working as expected

[isadofschi]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Inserting to an rb_map is not working as expected:

import init.meta
import order.basic

-- evaluates to [(4, 5), (2, 3)] as expected
#eval (((native.rb_map.of_list ([] : list (ℕ × ℕ))).insert 2 3).insert 4 5).to_list

-- evaluates to [(tt, 3), (ff, 5)] as expected
#eval (((native.rb_map.of_list ([] : list (bool × ℕ))).insert tt 3).insert ff 5).to_list

-- evaluates to [((ff, 4), 5)] instead of  [((tt, 2), 3), ((ff, 4), 5)]
#eval (((native.rb_map.of_list ([] : list ((bool × ℕ) × ℕ ))).insert (tt,2) 3).insert (ff,4) 5).to_list

Steps to Reproduce

1. This can be easily reproduced in gitpod with the latest mathlib.

Expected behavior: expression evaluates to [((tt, 2), 3), ((ff, 4), 5)]

Actual behavior: expression evaluates to [((ff, 4), 5)]

Reproduces how often: always

Versions

• On gitpod: Lean (version 3.44.1, commit 9d5adc6ab80d, Release) and mathlib 861589f224456f278c61596c0ee8a1ba449a6e8b

• On my PC (Ubuntu 20.04) Lean (version 3.42.1, commit 68455b087d87, Release)

[isadofschi]

Could this be happening because the order in bool × ℕ is not a total ordering?

Edit: yes, it seems that was the problem:

import init.meta
import order.lexicographic

#eval (((native.rb_map.of_list ([] : list ((bool ×ₗ ℕ) × ℕ ))).insert (tt,2) 3).insert (ff,4) 5).size

I don't know if we can require here that the ordering is a total order since rb_map is meta. For the "non meta" rbmap there seems to be a similar issue:

import order.basic

#eval (( (rbmap.from_list ([] : list ((bool×ℕ ) × ℕ))).insert (tt,2) 3).insert (ff,4) 5).to_list

If this is expected behaviour we probably want to document a reminder somewhere in mathlib_docs.

[fpvandoorn]

Feel free to make a PR that adds docstrings/module docs explaining that the ordering needs to be total. We can probably also change the definitions to require a linear_order, since the definition is nonsensical otherwise (incomparable elements are treated as equal, which is generally not a transitive relationship), but I'm not sure if that will have unfortunate side effects.