Duplicate Monad List instances about coq-ext-lib HOT 3 CLOSED

My understanding was that Data/Monads/ intends to provide monad instances of datatypes, while Data/List.v contains useful functions and lemmas over lists. @gmalecha please correct my misunderstandings.

One confusion is that List.v also contains instances other than monad, which don't fit elsewhere in the current setting, so it's unclear where to put definitions and instances. We could restructure the files if it helps addressing problems like universe inconsistency.

from coq-ext-lib.

I would prefer dropping ListMonad and similar modules when there is a corresponding Data/ module, that way Data/Monads/ is reserved for things whose usefulness is really derived from their monad instance.

from coq-ext-lib.

We could restructure the files if it helps addressing problems like universe inconsistency.

"Two instances" will add coherence problems if you mix the two abstractions.

OTOH, I'm no universe expert but "Two instances" won't add universe inconsistencies (it will add other problems), but Monad list will most likely add the same one as https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 (because template polymorphism is silly). Not sure if the other one is any better, but @Janno was skeptical.

from coq-ext-lib.