It would be good to have an option to return errors as erlang terms (when called from Erlang, not cli).

• various frontends can format the errors according to their taste (eg Elixir syntax formatting).
• also testing negative cases could be more precise

This requires unifying and documenting the error terms, each one having the same structure (common fields in same position: eg filename, line number, expected type etc.)

Also the default formatter (used by the cli) could have a format similar to other tools, like the compiler: file-name:line-number:error-text

The following code

-type t() :: #{year := integer() | nil,
	       price := integer() | nil,
	       model := 'Elixir.String':t() | nil}.

-spec 'can_buy?'('Elixir.Car':t(),
		 integer()) -> boolean().

'can_buy?'(#{price := Vprice@1}, Vmoney@1)
    when Vprice@1 =< Vmoney@1 ->
    true;
'can_buy?'(#{}, _) -> false.

currently not passing Gradualizer checks:

The pattern #{price := Vprice@1} on line 10 doesn't have the type 'Elixir.Car':t()

Is it bug or feature? I'm asking because big amount of Elixir code uses map-based types.

As a test to see how it ran, I ran Gradualizer on Gradualizer itself, there are a few issues, and they do seem to be legitimate:

╰─➤  find ebin/ -name '*.beam' -exec ./gradualizer -pa ebin {} \;                                                               127 ↵
ebin/gradualizer_db.beam: The function get_src_map on line 145 is expected to return #{module() => string()} but it returns #{module() => file:filename()}
ebin/gradualizer_db.beam: The pattern #{K := Types} on line 156 doesn't have the type #{mfa() => [type()]}
ebin/gradualizer_db.beam: The pattern #{K := TypeInfo} on line 271 doesn't have the type #{mfa() => #typeinfo{}}
ebin/gradualizer_db.beam: The pattern #{autoimport := false} on line 289 doesn't have the type opts()
ebin/gradualizer_db.beam: The pattern #{Mod := Filename} on line 308 doesn't have the type #{module() => string()}
ebin/gradualizer_db.beam: The pattern #{Mod := Filename} on line 320 doesn't have the type #{module() => string()}
ebin/gradualizer_db.beam: The variable 'Forms1' on line 343 has type {file:posix() | badarg | system_limit, file:filename()} |
          file:filename() |
          abstract_forms() but is expected to have type gradualizer_file_utils:abstract_forms()
escript: exception error: no match of right hand side value 
                 {{type,0,any,[]},
                  #{},
                  {constraints,#{},#{},
                               {set,0,16,16,8,80,48,
                                    {[],[],[],[],[],[],[],[],[],[],[],[],[],
                                     [],[],[]},
                                    {{[],[],[],[],[],[],[],[],[],[],[],[],[],
                                      [],[],[]}}}}}
  in function  typechecker:type_check_expr/2 (src/typechecker.erl, line 1005)
  in call from typechecker:type_check_expr/2 (src/typechecker.erl, line 906)
  in call from typechecker:type_check_block_in/3 (src/typechecker.erl, line 2023)
  in call from typechecker:type_check_block_in/3 (src/typechecker.erl, line 2024)
  in call from typechecker:check_clause/4 (src/typechecker.erl, line 2202)
  in call from lists:map/2 (lists.erl, line 1239)
  in call from typechecker:check_clauses/4 (src/typechecker.erl, line 2183)
  in call from typechecker:check_clauses_fun/3 (src/typechecker.erl, line 2153)
ebin/gradualizer_file_utils.beam: The tuple on line 28 does not have type parsed_file()
ebin/gradualizer_file_utils.beam: The tuple on line 37 does not have type parsed_file()
ebin/rebar_prv_gradualizer.beam: Undefined remote_type rebar_state:t/0 on line 8
ebin/rebar_prv_gradualizer.beam: Undefined remote_type rebar_state:t/0 on line 22
ebin/rebar_prv_gradualizer.beam: Undefined remote_type rebar_app_info:t/0 on line 32
ebin/rebar_prv_gradualizer.beam: Undefined remote_type rebar_app_info:t/0 on line 38
ebin/rebar_prv_gradualizer.beam: Call to undefined function rebar_dir:src_dirs/2 on line 71
ebin/typechecker.beam: The variable 'Tys' on line 366 has type [abstract_type()] |
          [abstract_type()] |
          [abstract_type()] |
          any |
          af_singleton_integer_type() |
          [(Name :: af_atom()) | af_record_field_type()] |
          [abstract_type()] |
          [af_assoc_type()] |
          any |
          [af_singleton_integer_type()] |
          af_function_type() |
          [{type, anno(), any} | abstract_type()] |
          [] |
          [] |
          [af_singleton_integer_type()] but is expected to have type [type()]
ebin/typechecker.beam: The tuple on line 597 does not have type int_range()
ebin/typechecker.beam: The tuple on line 615 does not have type type()
ebin/typechecker.beam: The tuple on line 781 does not have type any |
          {type_error, type()} |
          {fun_ty, type(), type(), constraints:constraints()} |
          {fun_ty_any_args, type(), constraints:constraints()} |
          {fun_ty_intersection, [type()], constraints:constraints()} |
          {fun_ty_union, [any()], constraints:constraints()}
ebin/typechecker.beam: The pattern {VEnv3,Cs2} on line 2246 doesn't have the type none() | none() | none() | any()
ebin/typelib.beam: The tuple on line 52 does not have type type()
ebin/typelib.beam: The operator '++' on line 97 is expected to have a non-list argument of type module() | file:filename()
ebin/typelib.beam: The tuple on line 129 does not have type type()

And it looks like there is a crash of Gradualizer itself within all that as well.

-module(plus).

-spec m(+1) -> {}.
m(+1) ->
    {}.

The pattern + 1 on line 4 doesn't have the type 1

Tying in with #56, it would be nice if I could open a PR which adds this test case as a known bug. Perhaps a known_problems/should_pass and known_problems/should_fail?

Coming from TypeScript I was curious why they choose to absorb T in T | any which becomes any.
The answer is simple: performance. Is there any literature on the implications of doing it as they do vs doing it as we do?

Is there a communication channel for just general discussion? I just wanted to have this in print and easily accessible - close when my meta question(s) are resolved!

Currently I'm investigating ability of using of this tool to analyze Elixir-compiled BEAM bytecode.
BEAM files compiled with Elixir compiler can be decompiled back to Erlang AST/source code.
Example: this file

https://github.com/coingaming/hm-crypto/blob/17dcf434c75e88506304343aafa9b63106d576a9/lib/hm_crypto/public_key.ex

Can be decompiled back to

-file("/Users/timcf/HTprojects/hm-crypto/lib/hm_cryp"
      "to/public_key.ex",
      1).

-module('Elixir.HmCrypto.PublicKey').

-compile(no_auto_import).

-spec parse_pem(rsa_key()) -> tuple().

-export_type([rsa_key/0]).

-type rsa_key() :: binary() | tuple().

-export(['__info__'/1, parse_pem/1]).

-spec '__info__'(attributes | compile | functions |
                 macros | md5 | module | deprecated) -> any().

'__info__'(module) -> 'Elixir.HmCrypto.PublicKey';
'__info__'(functions) -> [{parse_pem, 1}];
'__info__'(macros) -> [];
'__info__'(attributes) ->
    erlang:get_module_info('Elixir.HmCrypto.PublicKey',
                           attributes);
'__info__'(compile) ->
    erlang:get_module_info('Elixir.HmCrypto.PublicKey',
                           compile);
'__info__'(md5) ->
    erlang:get_module_info('Elixir.HmCrypto.PublicKey',
                           md5);
'__info__'(deprecated) -> [].

parse_pem(Vpem_string@1)
    when erlang:is_binary(Vpem_string@1) andalso
           Vpem_string@1 /= <<>> ->
    [Vpem_entry@1] = public_key:pem_decode(Vpem_string@1),
    public_key:pem_entry_decode(Vpem_entry@1);
parse_pem(Vpem@1) when erlang:is_tuple(Vpem@1) ->
    Vpem@1.

When I'm trying to apply Gradualizer to this file, first thing I get is error

The atom 'Elixir.HmCrypto.PublicKey' on line 24 does not have type Module

I'm not expert in pure Erlang standards, but isn't this atom a valid module name? If I run erl shell with loaded BEAM files of application - it works without any issues as module name:

Eshell V9.3.1  (abort with ^G)
1> 'Elixir.HmCrypto.PublicKey':parse_pem({hello, world}).
{hello,world}
2>

Any ideas about it?

A minimal example is:

-module(a).

-export([p/0]).

-spec p() -> ok.
p() -> ok.

-module(test).

-export([h/0]).

-import(a, [p/0]).

-spec h() -> ok.
h() -> p().

With Gradualizer producing:

test.erl: Call to undefined function p/0 on line 8

Hello, thanks for creating Gradualizer!
I tried it out on a simple module and ran into this error:

# foo.ex
defmodule Foo do
  @spec is_comment?(String.t()) :: boolean
  def is_comment?("#" <> _rest), do: true
  def is_comment?(_), do: false
end

iex(4)> :gradualizer.type_check_module(Foo)
The pattern <<"#",_rest@1/binary>> on line 3 doesn't have the type 'Elixir.String':t()
:nok

Looks like it hasn't resolved the type Elixir.String.t as a synonym for binary ?

Something is wrong with Erlang version?
Trying it with OTP20 / macos

Iljas-iMac:Gradualizer timcf$ make
erlc absform.erl
erlc constraints.erl
erlc gradualizer_db.erl
erlc typechecker.erl
typechecker.erl:5: Warning: export_all flag enabled - all functions will be exported
erlc typelib.erl
erl *.beam
2018-06-04 17:27:51 application_controller: ~ts: ~ts~n
	["syntax error before: ","'.'"]
	"absform.beam"
{"could not start kernel pid",application_controller,"{bad_environment_value,\"absform.beam\"}"}
could not start kernel pid (application_controller) ({bad_environment_value,"absform.beam"})

Crash dump is being written to: erl_crash.dump...done
make: *** [run] Error 1

These should all fail

-spec f(ok) -> ok.
f(10 = X) -> X.

-spec g(string()) -> ok.
g($a) -> ok.

-spec h(10..20) -> ok.
h(21) -> ok.

-spec i(integer()) -> ok.
i(1.0) -> ok.

   typechecker:handle_type_error({type_error,map,182,
                                                {type,227,term,[]}}) (src/typechecker.erl, line 2675)

And if you check typechecker.erl you see that a type_error,map is returned in 2 distinct places but is not handled in the error handler.

When I run make gradualize to gradualize the gradualizer itself, it crashes in typechecker.erl with the following error:

The variable 'Ty1' on line 60 has type type() but is expected to have type type()

I tried to solve it but I got confused. This is how far I got.

The first type() is defined in typechecker (the currently checked module) while the second is defined in typelib. (This can be seen by uncommenting some commented code in typelib:pp_type/1 which checks for filename annotation in the form and adds it to the output.)

So far so good. Next, to see what these type() expand to, I modified the exception caught in subtype/4 from nomatch to {nomatch, T1, T2} and the corresponding throw and printed out what exactly mismatches when comparing two types piece by piece. Now I can see that they are both normalized/expanded to {ann_type, anno(), [af_anno() | abstract_type()]} (where the types are local to erl_parse). There is no function clause in compat_ty for the case when both types are ann_type, but there is a clause that matches identical types compat_ty(T, T, A, _) -> ... which should match here. I don't understand why it doesn't match. I am confused.

What am I missing?

Test case:

%% -spec h(_) -> apple | banana.  % Same error with or without spec
h(1.0) -> banana;
h(_) -> apple.

Error

** exception error: no function clause matching typechecker:add_any_types_pat({float,14,1.0},#{}) (src/typechecker.erl, line 2542)
     in function  typechecker:add_type_pat/4 (src/typechecker.erl, line 2358)
     in call from typechecker:add_types_pats/4 (src/typechecker.erl, line 2348)
     in call from typechecker:check_clause/4 (src/typechecker.erl, line 2300)
     in call from lists:map/2 (lists.erl, line 1239)
     in call from typechecker:check_clauses/4 (src/typechecker.erl, line 2286)
     in call from typechecker:check_clauses_fun/3 (src/typechecker.erl, line 2256)
     in call from typechecker:'-type_check_forms/2-fun-0-'/5 (src/typechecker.erl, line 2680)

@gomoripeti in #53 wrote:

also could run make dialyze

Im not familiar with the new method and it probably needs to be done by a repo owner but would be nice to integrate travis with github PR checks (https://blog.travis-ci.com/2018-05-07-announcing-support-for-github-checks-api-on-travis-ci-com)

Would be nice if we follow up on that.

Given getenv/1 from OTP's os.erl:

-spec getenv(VarName) -> Value | false when
      VarName :: string(),
      Value :: string().

getenv(_) ->
    erlang:nif_error(undef).

The following code:

-spec get_so_path() -> binary() | string().
get_so_path() ->
    case os:getenv("EJABBERD_SO_PATH") of
        false ->
            case code:priv_dir(mongooseim) of
                {error, _} ->
                    ".";
                Path ->
                    filename:join([Path, "lib"])
            end;
        Path ->
            Path %% this is line 77
    end.

Results in:

The variable 'Path' on line 77 has type Value | false but is expected to have type binary() | string()

Which seems to be incorrect, since the first clause of the case rules out false, therefore Path must be a string(). I have a hunch this might be connected with this comment on type refinements, but my understanding of the theory is vague, to say the least :)

Surprisingly, the error persists in this case:

-spec get_so_path() -> binary() | string().
get_so_path() ->
    case os:getenv("APP_SO_PATH") of
        false ->
            "/fake/default/path";
        Path ->
            Path
    end.

But disappears when a binary literal is provided in the false clause:
It did disappear due to Vim not being able to parse a Gradualizer crash message.

-spec get_so_path() -> binary() | string().
get_so_path() ->
    case os:getenv("APP_SO_PATH") of
        false ->
            <<"/fake/default/path">>;
        Path ->
            Path
    end.

Checking the following file:

-module(docsh_internal).

-export([merge/1,
         kna/1]).

-export_type([t/0,
              item/0,
              kna/0]).

-type t()    :: #{name        := module(),
                  items       := [item()],
                  description => none | iodata()}.

-type item() :: #{kind        := function | type,
                  name        := atom(),
                  arity       := arity(),
                  description => none | iodata(),
                  exported    => boolean(),
                  signature   => iodata()}.

-type kna() :: {function | type, atom(), arity()}.

-define(a2b(A), atom_to_binary(A, utf8)).
-define(a2l(A), atom_to_list(A)).
-define(i2b(I), integer_to_binary(I)).
-define(il2b(IOList), iolist_to_binary(IOList)).

%%
%%' Public
%%

-spec merge([Info]) -> MergedInfo when
      Info :: t(),
      MergedInfo :: t().
merge([]) -> [];
merge([Info]) -> Info;
merge([Info1, Info2 | Rest]) ->
    case are_disjoint(Info1, Info2) of
        false -> erlang:error(not_disjoint, [Info1, Info2 | Rest]);
        true ->
            (module(Info1) =:= module(Info2)
             orelse erlang:error(different_modules, [Info1, Info2 | Rest])),
            merge([merge_two(Info1, Info2) | Rest])
    end.

-spec kna(item()) -> kna().
kna(#{kind := K, name := N, arity := A}) -> {K, N, A}.

%%.
%%' Internal
%%

-spec merge_two(t(), t()) -> t().
merge_two(#{items := Items1} = Info1, #{items := Items2}) ->
    ItemsByKNA = dict:to_list( docsh_lib:group_by(fun kna/1, Items1 ++ Items2) ),
    NewItems = lists:map(fun merge_two_/1,  ItemsByKNA),
    Info1#{items := NewItems}.

-spec merge_two_({kna(), [item()]}) -> item().
merge_two_({{Kind, Name, Arity}, [Item]}) ->
    #{kind := Kind, name := Name, arity := Arity} = Item,
    Item;
merge_two_({{Kind, Name, Arity}, [Item1, Item2]}) ->
    #{kind := Kind, name := Name, arity := Arity} = Item1,
    #{kind := Kind, name := Name, arity := Arity} = Item2,
    maps:merge(Item1, Item2).

are_disjoint(Info1, Info2) ->
    Module = maps:get(name, Info1),
    Module = maps:get(name, Info2),
    #{items := Items1} = Info1,
    #{items := Items2} = Info2,
    Items1 -- Items2 == Items1.

module(#{name := Name}) -> Name.

%%. vim: foldmethod=marker foldmarker=%%',%%.

I've run into the following error:

$ gradualizer src/docsh_internal.erl
src/docsh_internal.erl: The empty list on line 35 does not have type #{name := module(),
            items := [item()],
            description => none | iodata()}
escript: exception error: no match of right hand side value
                 #{'Dict' =>
                       [{user_type,[{file,"dict.erl"},{location,100}],
                                   dict,
                                   [{var,100,'Key'},{var,100,'Value'}]}],
                   'List' =>
                       [{type,101,list,
                              [{type,101,tuple,
                                     [{var,101,'Key'},{var,101,'Value'}]}]}]}
  in function  typechecker:solve_bounds/4 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1182)
  in call from typechecker:bounded_type_subst/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1166)
  in call from typechecker:expect_fun_type1/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1037)
  in call from typechecker:expect_intersection_type/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1095)
  in call from typechecker:expect_fun_type1/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1058)
  in call from typechecker:expect_fun_type/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1024)
  in call from typechecker:type_check_expr/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1315)
  in call from typechecker:type_check_expr/2 (/Users/erszcz/work/josefs/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 1234)

A trace on solve_bounds gives:

8> (<0.80.0>) call typechecker:solve_bounds({tenv,#{{item,0} =>
            {[],
             {type,14,map,
                   [{type,14,map_field_exact,
                          [{atom,14,kind},
                           {type,14,union,
                                 [{atom,14,function},{atom,14,type}]}]},
                    {type,15,map_field_exact,
                          [{atom,15,name},{type,15,atom,[]}]},
                    {type,16,map_field_exact,
                          [{atom,16,arity},{type,16,arity,[]}]},
                    {type,17,map_field_assoc,
                          [{atom,17,description},
                           {type,17,union,
                                 [{atom,17,none},{type,17,iodata,[]}]}]},
                    {type,18,map_field_assoc,
                          [{atom,18,exported},{type,18,boolean,[]}]},
                    {type,19,map_field_assoc,
                          [{atom,19,signature},{type,19,iodata,[]}]}]}},
        {kna,0} =>
            {[],
             {type,21,tuple,
                   [{type,21,union,[{atom,21,function},{atom,21,type}]},
                    {type,21,atom,[]},
                    {type,21,arity,[]}]}},
        {t,0} =>
            {[],
             {type,10,map,
                   [{type,10,map_field_exact,
                          [{atom,10,name},{type,10,module,[]}]},
                    {type,11,map_field_exact,
                          [{atom,11,items},
                           {type,11,list,[{user_type,11,item,[]}]}]},
                    {type,12,map_field_assoc,
                          [{atom,12,description},
                           {type,12,union,
                                 [{atom,12,none},{type,12,iodata,[]}]}]}]}}},
      #{}},#{'Dict' =>
      [{user_type,[{file,"dict.erl"},{location,100}],
                  dict,
                  [{var,100,'Key'},{var,100,'Value'}]}],
  'List' =>
      [{type,101,list,
             [{type,101,tuple,[{var,101,'Key'},{var,101,'Value'}]}]}]},[{acyclic,'Value'},{acyclic,'Key'},{acyclic,'List'},{acyclic,'Dict'}],#{})
(<0.80.0>) exception_from {typechecker,solve_bounds,4} {error,{badmatch,#{'Dict' =>
                       [{user_type,[{file,"dict.erl"},{location,100}],
                                   dict,
                                   [{var,100,'Key'},{var,100,'Value'}]}],
                   'List' =>
                       [{type,101,list,
                              [{type,101,tuple,
                                     [{var,101,'Key'},
                                      {var,101,'Value'}]}]}]}}}

My not so educated guess is that there's no complete support for maps or a bug there. Might it be the case?

There are modules in OTP which have really unfortunate type specs, from the point of view of Gradualizer. Take the function hd/1 for example. It has the following spec:

hd([term()]) -> term()

In Gradualizer, the type term() is the top of the subtyping hierarchy, which means that the code that consumes the output of hd/1 has to account for every kind of value there is! In practice it means that all uses of this function will signal a type error. That's no good! A better type would be:

hd([any()]) -> any()

One way to solve this problem is to provide our own type specs for problematic modules in OTP. We could instrument gradualizer_db to use its own set of specs instead of these modules.

A non-exhaustive list of problematic OTP modules

• lists
• proplists
• maps
• erlang
• mnesia
• ets
• qlc

(this ticket was split from #23 which also contain some of the early comments)

let's see the following correct function with spec

-spec f(atom() | integer()) -> true | integer().
f(AI) ->
    if is_atom(AI) ->    %% Expr1
         true;
       true ->
          AI + 1         %% Expr2
    end.

• the type of variable AI in Exrp2 must be the subtype of number() :: integer() | float() as the first argument of +
• the type of variable AI in Exrp2 is atom() | integer() based on the spec which is not a subtype of integer() | float()

How could Gradualizer realise that Expr2 is only executed when type of AI is integer()?

• if type checking was supersmart it would realise that if NOT is_atom(AI) => typeof(AI) == (atom() | integer()) & (not atom()) == integer() - however this is not always possible

Let's see a more generic example

-spec f(input()) -> any().
f(A) ->
  case cond(A) of
    true -> true;
    false -> body(A)
  end.

-spec cond(input()) -> boolean().
-spec body(required()) -> any().

In this case what the type checking could do is realise that body(A) is only executed in a subset of cases therefor type of A in body(A) is just a subset or subtype of input(). In case input() & required() == none() (the intersection of the two types is empty) then we can say that body(A) will always fail, but otherwise we cannot know (and have to leave type checking at runtime). This method requires to be able to calculate the intersection of two types.

What is the right way to handle these kind of constructs? (if, case, multiple function clause)

Currently the rules for pushing types into arithmetic operator applications in type_check_arith_op_in says (the other operator rules are similar):

  subtype(R, number)
  check(A, R)
  check(B, R)
  ------------------
  check(A op B, R)

This subtype constraint goes the wrong way, as shown in this example:

-spec f(integer(), integer()) -> integer() | divide_by_zero.
f(_X, 0) -> divide_by_zero;
f(X, Y)  -> X div Y.
%% The operator 'div' on line 8 is given a non-integer argument of type integer() | divide_by_zero

The error message is a bit strange as well, since it's the subtype(R, number) constraint that fails and not anything to do with the arguments.

The reason for having the subtyping this way around (I suspect) is to make this fail:

-spec g(number(), number()) -> integer().
g(X, Y) -> X + Y.
%% The variable 'X' on line 12 has type integer() | float() but is expected to have type integer()

I believe the correct rule is

  S = infer(A)
  T = infer(B)
  U = compat_arith_type(S, T)
  subtype(U, R)
  --------------------
  check(A op B, R)

Is the public API just the gradualizer module?
Is it fine that we use short module names like ty?

One of the discussions in #83 regards type assertions. A good idea that spawned out of that (thanks @zuiderkwast!) was that adding an id-function that accepts an extra dummy parameter representing a type would allow us to implement type assertions in an efficient and general way without the need to extend the language. To exemplify:

% defined in a header file, I suppose
assert_ty(V, _) -> V.

% Inferred spec: -spec foo(any()) -> integer().
foo(A) -> assert_ty(A, {type, integer}).

-spec bar(integer() | boolean()) -> integer().
% Trust me, due to "circumstances" I'm only ever called with integers...
bar(A) -> assert_ty(A, {type, integer}). 

To provide nicer syntax for type assertions @zuiderkwast suggests a parse transform:

I think it is possible to write a parse transform which allows us to write type annotations on this form: '::'(42, pos_integer()).
[...]
Example: A call to '::'([42], nonempty_list(pos_integer())) is transformed into '::'([42], {type, 0, nonempty_list, [{type, 0, pos_integer, []}]}.

Discussion points:

• What should the semantics of type assertions be? TypeScript sets a good precedence with their type assertion mechanism in that only "safe" type assertions are allowed without using "double assertion" via any. "Basically, the assertion from type S to T succeeds if either S is a subtype of T or T is a subtype of S".
• What should the syntax for types be? We need to limit ourselves to terms that are valid in any context, e.g. using any() to represent any() does not fly. Some ideas: the internal representation of types ('::'([42], {type, 0, nonempty_list, [{type, 0, pos_integer, []}]}), structured data that needs to be massaged (if we add some helper functions, e.g. type(T) -> {type, T}, this might turn out OK), or as a string (which we'll have to parse) e.g. '::'(42, "pos_integer()").

Currently the following code

-spec test() -> {atom1, atom2} | atom3.
test() ->
    case f() of
        {atom1, _} = X -> X;
        _ -> atom3
    end.

-spec f() -> {atom1, atom2} | atom4.
f() ->
    {atom1, atom2}.

gives me the error

The variable 'X' on line 7 has type {atom1, atom2} | atom4 but is expected to have type {atom1, atom2} | atom3

I want to work on making Gradualizer a real Erlang application so I'm wondering what you have in mind.
Is it a traditional long-running OTP application you have in mind or a CLI application that starts and stops between each request?
Perhaps an implementation using the Language Server Protocol?

I was happily surprised when Gradualizer pointed it out that I don't have to check for undefined if my function expects just t1/0 (BTW, I was writing production code - this is just a minimised example):

-module(test).

-export([f/1]).

-type t1() :: binary().

-spec f(t1()) -> ok | error | other.
f(T) ->
    case T of
        undefined -> error;
        _ -> other
    end.

However, it puzzled me way more when I changed the code to the following and got The pattern <<"ok">> on line 12 doesn't have the type undefined | <<_:_*8>> error:

-module(test).

-export([f/1]).

-type t1() :: binary().
-type maybe(T) :: undefined | T.

-spec f(maybe(t1())) -> ok | error | other.
f(T) ->
    case T of
        undefined -> error;
        <<"ok">> -> ok;
        _ -> other
    end.

I'm not sure if it's a known issue. It resembles #16 a bit, but that one is already closed.

Should Gradualizer support extended numeric types like non_neg_integer(), pos_integer() and others? Currently Gradualizer returns :nok in this example (Elixir)

  @spec factorial(non_neg_integer()) :: pos_integer()

  def factorial(0), do: 1
  def factorial(n) do
    n * factorial(n - 1)
  end

Error is

The operator '*' on line 7 is given a non-numeric argument  of type pos_integer()

Lager is probably the most popular logging framework used in the Erlang ecosystem. However, it's API is somewhat peculiar, because calling it is done with pseudo-calls, i.e. hooks which look like regular function calls, but are actually rewritten by lager_transform parse transformation. This results in, for example, Call to undefined function lager:debug/2 on line 204 messages.

One obvious way of solving this would be for a library using such a parse transformation to export properly typed function stubs. What's the Gradualizer team's stance on that? Do you suggest sending PRs adding suitable stubs e.g. to lager?

If module passed to &:gradualizer.type_check_module/1 function contains function calls to other modules, Gradualizer throws error Call to undefined function .... What is the proper way to avoid it?

This proposal is only about ergonomics and nothing to do with type-checker logic.
It was inspired by erl_types but slightly outdated by recent introduction of type/1/type/2 helper functions.

I propose to add helper macros like ?t_any/t_list([?t_integer]) etc, see gomoripeti@2e1b256 (this is an outdated commit but before the effort to rebase it I wanted to ask the team if it makes sense or I should just dismiss it forever)

pros:

• originally came up with this to avoid hassle with erl_anno:new(0) all over the place
• it also helps avoiding typos like type(tuple) when I really mean type(tuple, any) (equivalent with ?t_tuple)
• apart from constructing types (same usage as type/1/2 functions) it can also be used to match types ignoring second anno field (and optionally ignoring fourth field too)
• it gives a complete list for the gradualizer developer of what type() can be (and with an IDE also autocomplete can work quite nicely like ?t_<TAB>)

cons:

• handling the erl_parse type tuples as records is a hack, which is hidden by macros which is another hack

We have a reasonably good test suite with a lot of unit tests and a few test programs. It's very helpful and I use it all the time. But sadly, there are many cases that are not covered by the test suite. We can make it even more helpful! It'd be wonderful if people wanted to help out with this. It's also a very easy way to help out this project. I'm happy to assist anyone who wants to make a contribution.

When gradualizer is run as an escript (as on travis) it crashes with the below error:

{"init terminating in do_boot",{{badmatch,{error,enotdir}},
[{gradualizer_db,import_erl_files,2,[{file,"/home/travis/build/josefs/Gradualizer/_build/default/lib/gradualizer/src/gradualizer_db.erl"},{line,333}]},
 {gradualizer_db,init,1,[{file,"/home/travis/build/josefs/Gradualizer/_build/default/lib/gradualizer/src/gradualizer_db.erl"},{line,151}]}...

This can probably have something to do with code:priv_dir(gradualizer) => "/home/travis/build/josefs/Gradualizer/gradualizer/gradualizer/priv" because it is running from an escript archive.

(https://travis-ci.com/josefs/Gradualizer/jobs/156473749)

I've added a milestone called Beta release which right now collects some of the issues that I'd like to see resolved before we can announce a beta. My main goal is to have Gradualizer handle all language constructs in Erlang and not crash when invoked on syntactically valid programs.

I think we should aim at being lenient for the beta release and not report a type error if there is any doubt about what choice to make. We can refine the typing later.

I'm interested in hearing what people think of this plan and if there are other things you'd like to see in a beta.

First and foremost, I think this is a really great project! I especially like the speed it works with, since that makes it ideal for in-editor instant feedback.

I'm not sure if you're interested in this kind of reports at this stage - if not, please just ignore and close the issue. I've run Gradualizer on docsh and have got some crashes:

docsh_docs_v1.erl:
error: function_clause
stacktrace: [{typechecker,handle_type_error,
                 [{not_exported,remote_type,
                      {{atom,46,docsh_format},{atom,46,t},0}}],
                 [{file,"src/typechecker.erl"},{line,2640}]},
             {typechecker,'-type_check_forms/2-fun-0-',5,
                 [{file,"src/typechecker.erl"},{line,2544}]},
             {lists,foldr,3,[{file,"lists.erl"},{line,1276}]},
             {erl_eval,do_apply,6,[{file,"erl_eval.erl"},{line,670}]},
             {erl_eval,try_clauses,8,[{file,"erl_eval.erl"},{line,904}]},
             {erl_eval,exprs,5,[{file,"erl_eval.erl"},{line,122}]},
             {erl_eval,eval_lc1,6,[{file,"erl_eval.erl"},{line,696}]},
             {erl_eval,eval_generate,7,[{file,"erl_eval.erl"},{line,725}]}]

docsh_beam.erl:
error: function_clause
stacktrace: [{typechecker,type_check_expr,
                 ['*environment excluded*',
                  {remote,79,
                      {record_field,79,{var,79,'B'},docsh_beam,{atom,79,name}},
                      {atom,79,module_info}}],
                 [{file,"src/typechecker.erl"},{line,898}]},
             {typechecker,do_type_check_expr_in,3,
                 [{file,"src/typechecker.erl"},{line,1597}]},
             {typechecker,type_check_expr_in,3,
                 [{file,"src/typechecker.erl"},{line,1398}]},
             {lists,zipwith,3,[{file,"lists.erl"},{line,451}]},
             {lists,zipwith,3,[{file,"lists.erl"},{line,451}]},
             {typechecker,type_check_call,5,
                 [{file,"src/typechecker.erl"},{line,1924}]},
             {typechecker,do_type_check_expr_in,3,
                 [{file,"src/typechecker.erl"},{line,1598}]},
             {typechecker,type_check_expr_in,3,
                 [{file,"src/typechecker.erl"},{line,1398}]}]

docsh_syntax.erl:
error: function_clause
stacktrace: [{typechecker,do_type_check_expr_in,
                 ['*environment excluded*',
                  {var,1242,'Fun'},
                  {'fun',64,
                      {function,
                          {atom,64,docsh_syntax},
                          {var,64,'AttrName'},
                          {integer,64,1}}}],
                 [{file,"src/typechecker.erl"},{line,1401}]},
             {typechecker,type_check_expr_in,3,
                 [{file,"src/typechecker.erl"},{line,1398}]},
             {typechecker,'-type_check_call_ty/4-lc$^0/1-1-',2,
                 [{file,"src/typechecker.erl"},{line,1242}]},
             {typechecker,type_check_call_ty,4,
                 [{file,"src/typechecker.erl"},{line,1242}]},
             {typechecker,type_check_expr,2,
                 [{file,"src/typechecker.erl"},{line,975}]},
             {typechecker,type_check_lc,3,
                 [{file,"src/typechecker.erl"},{line,1343}]},
             {lists,map,2,[{file,"lists.erl"},{line,1239}]},
             {lists,map,2,[{file,"lists.erl"},{line,1239}]}]

You can run the checks from the gradualizer branch of docsh with make gradualizer.

I realise you might be aware of these - if so, I'm looking forward to all the future improvements!

Hi @josefs!

Thanks for the great presentation at EUC. After watching it, I had some questions and I thought I would reach out to you. I decided to open up an issue so other folks can jump into the discussion and contribute/learn. If this is not the proper medium or if you would prefer me to ask them elsewhere, please let me know and I will do it.

The first one is about any() and term(). In the presentation, you made it clear they are not the same. However, it is not clear to me what are the practical implications. Do you have an example of a typespec that would be pass with any() or not with term() and vice-versa?

The second question is about typing checking when calling untyped functions. Imagine you have:

-spec foo(integer(), integer()) -> integer().
foo(A, B) -> another_module:bar(A, B).

Where another_module:bar/2 is not spec'ed. Does it mean you assume another_module:bar/2 returns any() or do you perform partial evaluation in case another_module:bar/2 calls a typed function?

Thank you!

I've started work on integrating Gradualizer with Vim.

A Neomake maker runs the gradualizer EScript to obtain results for a file open in the current Vim buffer. The code path is extended with per-project ebin dirs, so that the analysis results are relatively accurate.

For now, the changes are available below - it still requires some polishing, so I'm not creating PRs yet:

• https://github.com/erszcz/Gradualizer/tree/vim-integration
• https://github.com/erszcz/neomake/tree/erlang-gradualizer

One thing that popped up in Gradualizer output is that line numbers are not placed consistently - I had to add a shell script to reformat them - that's the only change on the vim-integration branch above.

@josefs do you think this could be addressed directly in Gradualizer (likely gradualizer_cli.erl)? A format like this would be ideal (with on line 102 being redundant, but it doesn't hurt):

src/docsh_lib.erl:102: The type beam_lib:beam/0 on line 102 is not exported
src/docsh_lib.erl:114: The tuple on line 114 does not have type docsh_beam:debug_info() | false

In https://github.com/josefs/Gradualizer/pull/24#issuecomment-406861255` was mentioned that type_check_expr should not return type in any case (currently it return a type other than any if expr is fun objection, function call, expr with clauses (try, case, receive etc), record or tuple).
The general behaviour of type_check_expr is that it calls itself on subtypes of the expr and (maybe) type-checks the returned types. If the returned type is always any then what can this function check?

On a different note even type_check_expr_in calls type_check_expr to infer some type (eg in case Cond of Pattern -> ... Pattern is checked against the inferred type of Cond). Type checking could be more powerful if more precise type would be inferred for more expressions (eg a float literal could be inferred to be of type float())

But maybe the two functionalities could be split:

• type_check_expr checks the type of expression in case there is no type information available (basically same as checking against the any() type - checking a dynamic program)
• infer_type_of_expr would infer the type of the expression (this would have obviously limited scope and wouldn't go beyond the boundaries of function calls)

But I might misunderstand the roles of the functions (I ignored collecting constraints). What am I missing?

I believe type checking the return value of a function which is spec-ed to return term() should always pass (the same way as being spec-ed to return any()) as every type is a subtype of term(). (this is of course an under-specification from the side of the user)

This works fine for certain expressions where the subtype function is used, eg:

-spec return_float() -> term().
return_float() -> 1.23.

-spec return_string() -> term().
return_string() -> "asd".

However where the check uses the expect_*_type family of functions, type checking fails, because these helper functions don't allow term().

-spec return_tuple() -> term().
return_tuple() -> {1, 2}.

-spec return_list() -> term().
return_list() -> [1, 2].

-spec return_record() -> term().
return_record() -> #rec{}.

yields:

The tuple on line 48 does not have type term()
The expression [1,2] on line 51 does not have type term()
The record #rec on line 54 is expected to have type term().

I'm willing to fix this, if this is indeed a bug, however I'm not sure if the expect_*_type functions should be extended, or rather do_type_check_expr_in should short-circuit for term() the same way as for any()?

Currently gradualizer:type_check_file accepts files ending in .beam or .erl, however it would be nice to be able to give a BEAM forms term directly (type_check_forms?), perhaps other things like accepting an erlang string would be useful as well, however being able to pass in in-memory forms or a binary of a beam file (that may not exist on disk) would be very useful for tools built on this.

The function record_info/2 is a built-in pseudo-function. Currently, Gradualizer doesn't know about it and reports a type error. We need to add this function to the type environment.

The question is what type we should give this function. There is a whole spectrum of increasingly precise type we could give it. I'm considering whether we should try to make it as precise as possible by actually checking the arguments and return the actual fields or size, depending on how it's called.

For example, given the following record declaration:
-record(person, {name, phone, address}).
The call record_info(size, person) would have the singleton type 3.

In the JavaScript world, Flow and TypeScript can enable type checking on a per file basis in a project setup. This allows for gradual enabling of the type checker so that there is not an overwhelming amount of errors when starting out. Without a similar solution I think it will be difficult to add gradualizer to a big code base - especially if we do a good job with type inference.

The discussion about testing in #54 needs its own place.

Highlights:

@Zalastax:

What's your suggestion regarding testing? As you said, some code will fail/pass type checking depending on this option's value. Two new subdirectories?

@zuiderkwast:

I don't know @Zalastax. I think unit tests using code in strings, as in the typechecker_tests suite, is better than the should_fail/pass ones.

@Zalastax:

I don't agree that strings are better - they lack syntax highlighting.
Type checkers are a prime case for golden testing and I was happy to see that it's already what's being used. Golden testing is easier to reason about since every test case is completely static (less logic in test = good). We should only resort to unit tests with custom logic when it's absolutely necessary.

@gomoripeti:

regarding testing I think the should_pass/fail are nice as smoke tests but a bit limited (for example you cannot test if there are 1 or more errors in a should_fail module). the typechecker_tests-style tests need less context, can reach edge cases easier, or eg can also test specific errors (when gradualizer will support returning error terms)

regarding module attributes, I think in real use the option should be per project (eg in rebar.config) and not per module - but for testing a module attribute can be a nice idea.

Thoughts

My two personal goals are that:

• Tests should be easy to add and read (actual erlang files as tests score high here)
• Tests should not require lots of boilerplate/duplication (testing multiple errors for a module / testing small variations might be difficult if using actual erlang files)

I've had quite good success with the dtslint approach to testing types but I am not sure that's the path forward.

let's see the following correct function with spec

-spec f(atom() | integer()) -> true | integer().
f(AI) ->
    is_atom(AI)     %% Expr1
      orelse
        AI + 1.     %% Expr2

• the type of variable AI in Exrp2 must be the subtype of number() :: integer() | float() as the first argument of +
• the type of variable AI in Exrp2 is atom() | integer() based on the spec which is not a subtype of integer() | float()

How could Gradualizer realise that Expr2 is only executed when type of AI is integer()?

• if type checking was supersmart it would realise that if NOT is_atom(AI) => typeof(AI) == (atom() | integer()) & (not atom()) == integer() - however this is not always possible

Let's see a more generic example

-spec f(input()) -> any().
f(A) ->
  cond(A)
    orelse
      body(A).

-spec cond(input()) -> boolean().
-spec body(required()) -> any().

In this case what the type checking could do is realise that body(A) is only executed in a subset of cases therefor type of A in body(A) is just a subset or subtype of input(). In case input() & required() == none() (the intersection of the two types is empty) then we can say that body(A) will always fail, but otherwise we cannot know (and have to leave type checking at runtime). This method requires to be able to calculate the intersection of two types.

What is the right way to handle these kind of constructs? (if, case, andalso, orelse, multiple function clause)

I think we should aim for something very simple and permissive here. Perhaps all we should check is that the pattern matches against a binary string and ignore the sizes in the types, at least at first.

We have a decent test suite. It's be nice to leverage this by adding CI support. I have good experience with travis-ci but I'm interested in

We also have the possibility to run dialyzer if we implement CI support. Do people think that would be a good idea? I personally think it's be good to keep Gradualizer free from dialyzer warnings, but I'm too lazy to run it frequently. However, @gomoripeti runs it every now and again and finds useful improvements.

Attempting to run make escript on RedHat linux (which is locked to make version GNU Make 3.82 with no alternatives on the main installs), and running make escript gives this:

╰─➤  make escript
erlang.mk:30: Please upgrade to GNU Make 4 or later: https://erlang.mk/guide/installation.html
erlang.mk:30: Please upgrade to GNU Make 4 or later: https://erlang.mk/guide/installation.html
 GEN    escript-zip

WARNING: No more files
gradualizer

make: *** [escript-zip] Error 1

And the supplied link is useless as it says nothing about how to workaround the issue on modern RedHat installs (which regulate what can and cannot be installed).

A function can have multiple specs, which the documentation calls overloading and whose semantics is intersection types. For instance,

-spec foo(boolean()) -> its_a_bool;
         (integer()) -> its_an_int.

means that foo has both the type boolean() -> its_a_bool and the type integer() -> its_an_int.

We currently handle this for function definitions and explicit calls using the fun_ty_intersection return value from expect_fun_type, but not for fun F/A and fun M:F/A expressions. To do this we'd need to be able to represent intersection types in the type language.

Hello!

I was wondering if there would be any interest in/possibility of adding Elixir support to Gradualizer?

Semantically they are near identical languages that use the same typespecs, so I feel the same tool could be applied to both. I can think of two main differences:

1. Elixir has Lisp style macros. To handle this type checking could be performed after macro resolution so no knowledge of that system is required.

2. Elixir has protocols, which are slightly similar to Haskell's typeclasses and have no equivalent in Erlang. This could be ignored, at least to start.

I've not yet read any of the Gradualizer source- does this feature seem realistic and achiveable?

Cheers,
Louis

typechecker:handle_type_error({type_error,bin,0,           
                                                              {user_type,[{file,"test_path.erl"},{location,24}],t,[]}}) (/home/overminddl1/erlang/gradualizer/_build/default/lib/gradualizer/src/typechecker.erl, line 2807)

It seems binary types are not being handled by the type error path? So should be a simple fix. Although the fact that the binary is not passed in like it is for strings/charlists seems odd? Also typelib:pp_type(Ty) does not seem to add the remote module name to the type so I just get something like t() instead of test_path:t() or so, and with how common t is as a type name that's not terribly helpful, plus just seeing t isn't really helpful either, it would be nice to get a list of types drilled down. :-)

While running gradualizer on an a mature Elixir project, I got quite a few of these:

*********************************
Report this error to Gradualizer:

** (FunctionClauseError) no function clause matching in :typechecker.handle_type_error/1

The following arguments were given to :typechecker.handle_type_error/1:

    # 1
    {:type_error, :map, 151, {:type, 141, :union, [{:atom, 0, nil}, {:user_type, 141, :attract_file, []}]}}

    /Users/jowens/dev/snoke/deps/gradualizer/src/typechecker.erl:3327: :typechecker.handle_type_error/1
    /Users/jowens/dev/snoke/deps/gradualizer/src/typechecker.erl:3228: anonymous fn/5 in :typechecker.type_check_forms/2
    (stdlib) lists.erl:1276: :lists.foldr/3
    lib/gradualixir.ex:37: anonymous fn/2 in Gradualixir.gradualize/2
    (elixir) lib/enum.ex:3281: Enumerable.List.reduce/3
    (elixir) lib/enum.ex:1968: Enum.reduce_while/3
    lib/mix/tasks/gradualizer.ex:25: Mix.Tasks.Gradualizer.run/1
    (mix) lib/mix/task.ex:316: Mix.Task.run_task/3
    (mix) lib/mix/cli.ex:79: Mix.CLI.run_task/2
    (elixir) src/elixir_compiler.erl:71: :elixir_compiler.dispatch/4
    (elixir) src/elixir_compiler.erl:68: :elixir_compiler.compile/3
    (elixir) src/elixir_lexical.erl:17: :elixir_lexical.run/2
    (elixir) src/elixir_compiler.erl:23: :elixir_compiler.quoted/2
    (elixir) lib/code.ex:767: Code.require_file/2
    (elixir) lib/kernel/cli.ex:503: Kernel.CLI.wrapper/1
    (elixir) lib/enum.ex:1314: Enum."-map/2-lists^map/1-0-"/2
    (elixir) lib/kernel/cli.ex:68: Kernel.CLI.process_commands/1
    (elixir) lib/kernel/cli.ex:26: anonymous fn/2 in Kernel.CLI.main/1
    (elixir) lib/kernel/cli.ex:105: anonymous fn/3 in Kernel.CLI.exec_fun/2

I was using https://github.com/OvermindDL1/gradualixir

Sorry, I couldn't figure out quickly what is wrong so just reporting it.
(I suspect something around expect_tuple_type returning {type, 0, any, []} instead of any)

Type checking the below program

-spec f(tuple() | integer()) -> ok.
f({1, 2}) ->
    ok.

results in the below crash

escript: exception error: no function clause matching
                 lists:zip([{integer,2,1},{integer,2,2}],{type,0,any,[]}) (lists.erl, line 387)
  in function  typechecker:add_type_pat/4 (src/typechecker.erl, line 2117)
  in call from typechecker:add_types_pats/4 (src/typechecker.erl, line 2093)
  in call from typechecker:check_clause/4 (src/typechecker.erl, line 2032)
  in call from lists:map/2 (lists.erl, line 1239)
  in call from typechecker:check_clauses/4 (src/typechecker.erl, line 2018)
  in call from typechecker:type_check_function/2 (src/typechecker.erl, line 2080)
  in call from typechecker:'-type_check_forms/2-fun-0-'/5 (src/typechecker.erl, line 2358)