Unsound refinements

[ilya-klyuchnikov]

Example:

-module(ex).

-export([example/1]).

-spec example({a, atom()} | {i, integer()}) -> atom().
example({i, I}) when I > 0 -> integer;
example({_, A}) -> A.

gradualizer unsoundly accepts this code, - while example({i, 0}) ==> 0.

I guess that for the first clause gradualizer mistakenly infers that {i, integer()} tagged tuple argument is completely covered by the clause, while it is not.

[zuiderkwast]

Bug! This is not at all intended.

IIRC, initially when we added refinement, there was a condition on no guards for refinement to happen. Later, we extended it to allow refinement with certain simple guards, such as I > 0, so that we could exclude pos_integer() in this case. I'm not sure why it's not working in this example.

[erszcz]

Confirmed, still a bug as of now:

$ ./bin/gradualizer --version
Gradualizer v0.1.3-145-gab75f28
$ cat > ex.erl
-module(ex).

-export([example/1]).

-spec example({a, atom()} | {i, integer()}) -> atom().
example({i, I}) when I > 0 -> integer;
example({_, A}) -> A.
$ ./bin/gradualizer ex.erl
$ 

No type errors reported :|