New gmap representation causes set_solver / reflexivity to diverge

When porting DimSum to !461 (merged), I noticed that some calls to set_solver diverge now whereas they used to succeed before. In particular, the following goal used by the solved by set_solver but it is not solved by it anymore as the new definition of gmap causes reflexivity to diverge:

Goal dom ((<["f":=1]> ∅) : gmap _ _) = dom ((<["f":=2]> ∅) : gmap _ _).
Proof.  
  Fail Timeout 2 set_solver.
  Fail Timeout 2 reflexivity.
  vm_compute. reflexivity.
Qed.