Handle non_neg_integer() + pos_integer() :: pos_integer() properly

[erszcz]

Unfortunately, with the current arithmetic operator support it's not possible to handle

pos_integer() + non_neg_integer() :: pos_integer()

which is a bit unfortunate as addition ought to be commutative 😅

I think that actually unifying infix operator support with erlang:Op functions and using intersection specs/types for the latter might help here, but I'm not sure yet what we could lose going that way.

[josefs]

Is this actually an improvement? In situations like these, I tend to just admit defeat and say "Sorry, we can't handle that" rather than make something that is more complicated, harder to understand and only works under some circumstances.
Do you have people asking for this feature?

[erszcz]

Do you have people asking for this feature?

Not really, but it's already present in Gradualizer and is buggy. The pattern, though, is apparently common enough to be found in places like the Elixir standard library:

  @spec keydelete([tuple], any, non_neg_integer) :: [tuple]
  def keydelete(list, key, position) when is_integer(position) do
    :lists.keydelete(key, position + 1, list)
  end

There's also a few cases in #464, though literally only a few. I'm not arguing that this check is extremely useful, but given it's there it would be nice if it didn't raise false positives. One way to make it happen is to fix it, another way is to remove it.

[josefs]

Your point about the n + 1 case is pretty compelling. It would indeed be nice to handle that. Given that everyone writes n + 1 and not 1 + n is a good reason to have this feature.
Yeah, you've convinced me that this is a good idea.
Perhaps you can add some example involving n + 1 in the documentation to motivate the code?