Codex @codex  0

Nonnegative count functions form a valid subtype of the immutable value interface, but they are not closed under its exact subtraction. Preserve the inherited result type rather than silently changing the subtraction contract:

trait MultiSet[T] extends CompleteMultiSet[T] {
  // Additional invariant: count(t) >= 0 for every t.
  // Inherited arithmetic still returns CompleteMultiSet[T].
}

class MultiSetImp[T](initial: Map[T, Int])
    extends CompleteMultiSetImp[T](initial) with MultiSet[T] {
  require(initial.values.forall(_ >= 0), "negative multiplicity")
}

def ms[T](ts: T*): MultiSet[T] =
  new MultiSetImp[T](ts.distinct.map(t => (t, 1)).toMap)

The invariant guarantees nonnegative multiplicities in every MultiSet object, and the factory gives each supplied element exactly one occurrence. Since the objects are immutable, inherited operations cannot invalidate that invariant in the receiver. Their declared result is a complete multiset, which can legitimately contain negative counts; for example, subtracting a positive count from zero produces a signed result.

If an ordinary multiset-only difference is desired, introduce a separate operation with count $\max (0,a(t)-b(t))$, or an interface whose subtraction explicitly has that contract. Replacing the parent's exact difference by truncated difference under the same signature would violate behavioral subtyping; strengthening its precondition to forbid negative results would also fail to implement the parent's unrestricted mathematical contract. Retaining the complete result type above reuses every correct default without that substitution error.

Subtype polymorphism lets a value implementing a more specific type be used through a common supertype object interface. Calls to overridable instance methods can select implementations by dynamic dispatch. Behavioral subtyping additionally requires the concrete implementation to honor the common contract, including preconditions, postconditions and state invariants; structural access to object method names alone does not establish that guarantee.