Binary type inference is stricter than it needs to be

[mtshiba]

Describe the bug?

No response

Reproducible code

add1 x = 1 + x
y = add1 3.1

Expected result

passed.

Actual result

Error[#1259]: File test.er, line 2, <module>::x

2 | y = add1 3.1
  :          ---
  :             |- expected: Nat
  :             `- but found: {3.1f, }

the type of add1::x (the 1st argument) is mismatched

Additional context

add1 should be type of |T: Type, Nat <: U <: Add(T)| T -> U.Output, but inferred to be Nat -> Nat.

Erg version

0.6.0-beta.2

Python version

No response

OS

None