erg-lang / erg

A statically typed language compatible with Python
http://erg-lang.org
Apache License 2.0
2.61k stars 53 forks source link

`sum` with refinement types #496

Open mtshiba opened 3 months ago

mtshiba commented 3 months ago

Describe the bug?

If you substitute an expression with a dependent type to the argument of sum, the return type will be wrong.

Reproducible code

s: {2, 1} = sum [1, 2]

Expected result

TypeError: sum([1, 2]): Nat (or {3})

Actual result

passed

Additional context

Here is the type definition of sum:

|A <: Add(A)| (iterable: Iterable(A), start: A or Int := Int) -> A

Erg version

0.6.32

Python version

None

OS

None