gset has a non-trivial universe constraints

I just noticed that gset lives in Type@{max(Set,gmap.u1)} and there seem to nontrivial universe constraints. In particular, together with importing ExtLib (which does not use stdpp) we get the constraint gmap.u1 = sum.u1 (and gmap.u1 <= sum.u0). This leads to universe errors later when using gset inside itrees. Where does this constraint come from? Is there a way to fix this?

From ExtLib Require Import
     Data.Monads.OptionMonad
     Data.Monads.EitherMonad.
Require Export stdpp.gmap.
Set Printing Universes.
Print gset.
(* => gset = 
λ (K : Type@{gset.u0}) (EqDecision0 : EqDecision K) (H : Countable K), mapset.mapset (gmap K)
     : ∀ (K : Type@{gset.u0}) (EqDecision0 : EqDecision K), Countable K → Type@{max(Set,gmap.u1)}
*)
Constraint sum.u1 < gmap.u1.
(* => Error: Universe inconsistency. Cannot enforce sum.u1 < gmap.u1 because gmap.u1 = sum.u1. *)

One work around seems to be to use gmap K () instead of gset as gmap lives in Set.