I’m writing a multiset library. It’s got 2 modules: one which works on raw “multisets” (which are maps of elements to quantities), and another which is just a Struct type wrapping the same functionality in much nicer ergonomics.

For the former module, all the methods support so-called “lax” multisets, where some element => 0 records may be included; but many methods include a strict \\ :lax :: :lax | :strict parameter that can be used to switch on better codepaths whenever the caller can guarantee the multiset isn’t “lax”.

I’m trying to write the type system to support that, so that Dialyzer will be helpful to any consumers. However, the type signature for one method, delete, has turned out suspiciously verbose; I’m wondering if there’s any way to shore this up with some syntax that more clearly semantically indicates “this type in the output is the same as this type in the input, and said type must in any case fit some constraint, and you should try fitting the allowed types in this particular priority order”, without this combinatorial explosion:

@type t(value) :: %{optional(value) => pos_integer()}
@type t() :: t(term)

@type t_lax(value) :: %{optional(value) => non_neg_integer()}
@type t_lax() :: t_lax(term)

@type t0(value) :: Enumerable.t({value, non_neg_integer()})
@type t0() :: t0(term)

# …

@spec delete(t(e), term) :: t(e) when e: term # non-lax output is guaranteed from non-lax input
@spec delete(t_lax(e), term) :: t_lax(e) when e: term
@spec delete(t(e), term, :all) :: t(e) when e: term # non-lax output is guaranteed from non-lax input
@spec delete(t_lax(e), term, :all) :: t_lax(e) when e: term
@spec delete(t(e), term, non_neg_integer()) :: t(e) when e: term # non-lax output is guaranteed from non-lax input
@spec delete(t_lax(e), term, non_neg_integer()) :: t_lax(e) when e: term
def delete(ms, element, count)

def delete(ms, element, :all), do: Map.delete(ms, element)

def delete(ms, element, count) when is_pos_integer(count) do
  case ms do
    %{^element => n1} ->
      n2 = n1 - count

      if n2 > 0 do
        %{ms | element => n2}
      else
        Map.delete(ms, element)
      end

    %{} ->
      ms
  end
end

def delete(ms, _, 0), do: ms