WhatsApp / eqwalizer

A type-checker for Erlang
Apache License 2.0
506 stars 27 forks source link

Missed type errors #12

Closed duncanatt closed 1 year ago

duncanatt commented 1 year ago

I am experimenting with eqWAlizer on the code below, expecting it to complain.

-spec inc_1(atom()) -> integer().
inc_1(X) when is_integer(X) -> X + 1.

However, no error is flagged. Similarly, no error is raised for this function:

-spec inc_2(integer()) -> integer().
inc_2(X) when is_atom(X) -> X + 1.

Once the guards are removed from the above functions, the expected behaviour is obtained (i.e. an error is flagged in the case of inc_1, whereas inc_2 type checks).

I also noticed that this type checks:

-spec int_error(float(), float()) -> integer().
int_error(X, Y) ->
    X div Y.

Is there something that I am missing, please?

VLanvin commented 1 year ago

The first two functions being accepted is to be expected. If X is of type atom(), then is_integer(X) always fails, and the branch cannot be chosen at runtime. Therefore, there is no point in checking its type. In more technical terms, the guard is_integer(X) refines the type of X from atom() to none(), which makes X + 1 well-typed.

Regarding the second function, eqWAlizer simply does not differentiate between numeric types, it simply assumes them all to be number(). Hence, your spec is equivalent (from eqWAlizer's POV) to -spec int_error(number(), number()) -> number(). This is a design choice we made for technical and simplicity reasons.