Skip to content

There are two "SubsetEq" instances for gmultiset

We currently have two non-equivalent instances for SubsetEq for gmultiset, which leads to very confusing situations:

  • gmultiset_subseteq is the expected instance in terms of multiplicites
  • But there also is set_subseteq which is a general instance based on ElemOf.

IMO multisets show that the general instance is undesirable -- from the fact that a type has an ElemOf instance, we cannot derive how its subset relation ought to look. That instance should likely be removed, and replaced by manual instances for types that actually want it.

FWIW, the same applies to the general set_equiv. I am not sure about set_disjoint... that one is correct for multisets, so maybe we can keep it at least for now. "No element is in both sets" seems like a reasonable definition for disjointness for anything that has membership.