Duplicate Monad List instances

[Blaisorblade]

One is in https://github.com/coq-community/coq-ext-lib/blob/master/theories/Data/Monads/ListMonad.v and one is in https://github.com/coq-community/coq-ext-lib/blob/master/theories/Data/List.v#L1-L123, and they're differently polymorphic.

(We noticed while wondering with @Janno whether ext-lib suffers from https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80, and whether that causes MetaCoq/metacoq#580, but I'm not sure either way; at least ListMonad.v looks suspicious — and MetaCoq/metacoq#580 (comment) discusses the universe problem).

[liyishuai]

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.

[Lysxia]

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.

[Blaisorblade]

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.