stdpp constrains the template universe `list.u0` (and many others)

We've known about this issue for quite a while (since September 2017, to be precise) and the Mtac2 project has worked around this issue by creating a copy of the standard library, i.e. by (almost) never using list. Of course, that is a good thing to do anyway since template polymorphic types are broken beyond repair.

The current state, as far as I can see, is that stdpp basically equates the template universes of all inductive datatypes that implement MRet, MJoin, and the various other classes. People are unfortunate enough to have to debug these things might be familiar with stdpp.base.663 (universe name might differ; it's the first universe of MRet) which shows up everywhere.

The reason that all of this doesn't constantly explode is that a) most datatypes are as big as their contents (in terms of universes) and b) nobody seems to be putting large datatypes in other datatypes. So we end up with exactly one universe into which everything has to fit.

I am now working on (non-Mtac2) iris code in which I can no longer work around this problem. I cannot share the code but the setup is roughly this: I compute a list iProp using (among other things) bi_texist. In another place, but with this construction in scope, I want to write bi_texist (TT:=[tele P:iProp]) but I no longer can because of the universe constraints imposed by stdpp.

Slightly more concrete code sketch that demonstrates the problem:

From iris Require Import iprop telescopes fancy_updates.
Section with_Σ.
  Context `{Σ : gFunctors}.
  Set Printing Universes.
  Definition bla : list _ := (bi_texist (PROP:=iPropI Σ) (TT:=[tele (n:nat)])) :: nil.
  Fail Definition t := bi_texist (PROP:=iPropI Σ) (TT:=[tele (P:iPropI Σ)]).

I am sure we can come up with a non-iris example to break things. (A list MRet would probably do it. But that seems even more contrived than the code above.)

It is not clear what to do exactly. In particular, it is not at all clearer what to do now than it was 3 years ago. One way or another stdpp will have to move away from template polymorphic datatypes. There have been some improvements to universe polymorphism in Coq so maybe a fork of the standard library is more possible now than it was before?