Remove the --infer option

This removes the --infer CLI and #env{} option.
The Erlang VM does dynamic type checking based on type tags embedded in values.
This means that it's safe to infer type information from literals and operators
according to the same rules that the VM enforces at runtime.
Actually, these are one of the few completely credible sources of information,
unlike type specs, in which there's room for human error.
Removing the option along with the branching in the typechecker should somewhat
minimise the amount of code to maintain.

Makefile

@@ -90,7 +90,7 @@ bin/gradualizer: $(beams) ebin/gradualizer.app
 
 .PHONY: gradualize
 gradualize: escript
-	@bin/gradualizer --infer --solve_constraints --specs_override_dir priv/extra_specs/ \
+	@bin/gradualizer --solve_constraints --specs_override_dir priv/extra_specs/ \
         -pa ebin --color ebin | grep -v -f gradualize-ignore.lst
 
 .PHONY: nocrashongradualize

src/gradualizer.erl

@@ -425,7 +425,6 @@ type_of(Expr) ->
 %% '''
 -spec type_of(string(), typechecker:env()) -> typechecker:type().
 type_of(Expr, Env) ->
-    AlwaysInfer = Env#env{infer = true},
     [Form] = gradualizer_lib:ensure_form_list(merl:quote(lists:flatten(Expr))),
-    {Ty, _Env} = typechecker:type_check_expr(AlwaysInfer, Form),
+    {Ty, _Env} = typechecker:type_check_expr(Env, Form),
     Ty.

src/gradualizer_cli.erl

@@ -70,10 +70,7 @@ print_usage() ->
     io:format("                                 arguments are treated as filenames, even if~n"),
     io:format("                                 they start with hyphens.~n"),
     io:format("  -h,  --help                    display this help and exit~n"),
-    io:format("       --infer                   Infer type information from literals and other~n"),
     io:format("                                 language constructs~n"),
-    io:format("       --no_infer                Only use type information from function specs~n"),
-    io:format("                                  - the default behaviour~n"),
     io:format("       --verbose                 Show what Gradualizer is doing~n"),
     io:format("  -pa, --path_add                Add the specified directory to the beginning of~n"),
     io:format("                                 the code path; see erl -pa             [string]~n"),
@@ -109,8 +106,6 @@ parse_opts([A | Args], Opts) ->
     case A of
         "-h"                       -> {[], [help]};
         "--help"                   -> {[], [help]};
-        "--infer"                  -> parse_opts(Args, [infer | Opts]);
-        "--no_infer"               -> parse_opts(Args, [{infer, false} | Opts]);
         "--verbose"                -> parse_opts(Args, [verbose | Opts]);
         "-pa"                      -> handle_path_add(A, Args, Opts);
         "--path_add"               -> handle_path_add(A, Args, Opts);

src/typechecker.erl

@@ -1869,26 +1869,13 @@ do_type_check_expr(Env, {'case', _, Expr, Clauses}) ->
     {Ty, union_var_binds(Env1, VB, Env)};
 do_type_check_expr(Env, {tuple, _, TS}) ->
     {Tys, VarBindsList} = lists:unzip([ type_check_expr(Env, Expr) || Expr <- TS ]),
-    InferredTy =
-        case not Env#env.infer andalso
-             lists:all(fun({type, _, any, []}) -> true;
-                          (_) -> false
-                       end, Tys) of
-            true ->
-                type(any);
-            false ->
-                %% at least one element in the tuple has a type inferred from a spec
-                type(tuple, Tys)
-        end,
+    InferredTy = type(tuple, Tys),
     {InferredTy, union_var_binds(VarBindsList, Env)};
 do_type_check_expr(Env, {cons, _, Head, Tail}) ->
     {Ty1, VB1} = type_check_expr(Env, Head),
     {Ty2, VB2} = type_check_expr(Env, Tail),
     VB = union_var_binds(VB1, VB2, Env),
     case {Ty1, Ty2} of
-        {?type(any), ?type(any)} when not Env#env.infer ->
-            %% No type information to propagate
-            {type(any), VB};
         {_, ?type(any)} ->
             %% Propagate type information from head
             {type(nonempty_list, [Ty1]), VB};
@@ -1922,14 +1909,8 @@ do_type_check_expr(Env, {bin, _, BinElements} = BinExpr) ->
                           type_check_expr_in(Env, Ty, Expr)
                   end,
                   BinElements),
-    RetTy = if
-                Env#env.infer ->
-                    %% Infer the size parameters of the bitstring
-                    gradualizer_bin:compute_type(BinExpr);
-                not Env#env.infer ->
-                    type(any)
-            end,
-    RetTy = ?assert_type(RetTy, type()),
+    %% Infer the size parameters of the bitstring
+    RetTy = gradualizer_bin:compute_type(BinExpr),
     {RetTy, union_var_binds(VarBinds, Env)};
 do_type_check_expr(Env, {call, _, {atom, _, TypeOp}, [Expr, {string, _, TypeStr} = TypeLit]})
   when TypeOp == '::'; TypeOp == ':::' ->
@@ -1975,46 +1956,24 @@ do_type_check_expr(Env, {bc, _, Expr, Qualifiers}) ->
 do_type_check_expr(Env, {block, _, Block}) ->
     type_check_block(Env, Block);
 
-% Don't return the type of anything other than something
-% which ultimately comes from a function type spec.
-do_type_check_expr(#env{infer = false} = Env, {string, _, _}) ->
-    {type(any), Env};
-do_type_check_expr(#env{infer = false} = Env, {nil, _}) ->
-    {type(any), Env};
-do_type_check_expr(#env{infer = false} = Env, {atom, _, _Atom}) ->
-    {type(any), Env};
-do_type_check_expr(#env{infer = false} = Env, {integer, _, _N}) ->
-    {type(any), Env};
-do_type_check_expr(#env{infer = false} = Env, {float, _, _F}) ->
-    {type(any), Env};
-do_type_check_expr(#env{infer = false} = Env, {char, _, _C}) ->
-    {type(any), Env};
-
-%% When infer = true, we do propagate the types of literals,
-%% list cons, tuples, etc.
-do_type_check_expr(#env{infer = true} = Env, {string, _, Chars}) ->
+do_type_check_expr(Env, {string, _, Chars}) ->
     ActualTy = infer_literal_string(Chars, Env),
     {ActualTy, Env};
-do_type_check_expr(#env{infer = true} = Env, {nil, _}) ->
+do_type_check_expr(Env, {nil, _}) ->
     {type(nil), Env};
-do_type_check_expr(#env{infer = true} = Env, {Tag, _, Value})
+do_type_check_expr(Env, {Tag, _, Value})
   when Tag =:= atom;
        Tag =:= integer;
        Tag =:= char ->
     {singleton(Tag, Value), Env};
-do_type_check_expr(#env{infer = true} = Env, {float, _, _F}) ->
+do_type_check_expr(Env, {float, _, _F}) ->
     {type(float), Env};
 
 %% Maps
 do_type_check_expr(Env, {map, _, Assocs}) ->
     {AssocTys, VB} = type_check_assocs(Env, Assocs),
-    case Env#env.infer of
-        true ->
-            MapTy = update_map_type(type(map, []), AssocTys),
-            {MapTy, VB};
-        false ->
-            {type(any), VB}
-    end;
+    MapTy = update_map_type(type(map, []), AssocTys),
+    {MapTy, VB};
 do_type_check_expr(Env, {map, _, UpdateExpr, Assocs}) ->
     {Ty, VBExpr} = type_check_expr(Env, UpdateExpr),
     {AssocTys, VBAssocs} = type_check_assocs(Env, Assocs),
@@ -2058,14 +2017,9 @@ do_type_check_expr(Env, {record, Anno, Record, Fields}) ->
     VB = type_check_fields(Env, Rec, Fields),
     {RecTy, VB};
 do_type_check_expr(Env, {record_index, Anno, Name, FieldWithAnno}) ->
-    case Env#env.infer of
-        true ->
-            RecFields = get_record_fields(Name, Anno, Env),
-            Index = get_rec_field_index(FieldWithAnno, RecFields),
-            {{integer, erl_anno:new(0), Index}, Env};
-        false ->
-            {type(any), Env}
-    end;
+    RecFields = get_record_fields(Name, Anno, Env),
+    Index = get_rec_field_index(FieldWithAnno, RecFields),
+    {{integer, erl_anno:new(0), Index}, Env};
 
 %% Functions
 do_type_check_expr(Env, {'fun', _, {clauses, Clauses}}) ->
@@ -2097,16 +2051,11 @@ do_type_check_expr(Env, {'fun', P, {function, M, F, A}}) ->
 do_type_check_expr(Env, {named_fun, _, FunName, Clauses}) ->
     %% Pick a type for the fun itself, to be used when checking references to
     %% itself inside the fun, e.g. recursive calls.
-    FunTy = if
-                Env#env.infer ->
-                    %% Create a fun type of the correct arity
-                    %% on the form fun((_,_,_) -> any()).
-                    [{clause, _, Params, _Guards, _Block} | _] = Clauses,
-                    Arity = arity(length(Params)),
-                    create_fun_type(Arity, type(any));
-                not Env#env.infer ->
-                    type(any)
-            end,
+    %% Create a fun type of the correct arity
+    %% on the form fun((_,_,_) -> any()).
+    [{clause, _, Params, _Guards, _Block} | _] = Clauses,
+    Arity = arity(length(Params)),
+    FunTy = create_fun_type(Arity, type(any)),
     NewEnv = add_var_binds(Env#env{venv = #{FunName => FunTy}}, Env, Env),
     type_check_fun(NewEnv, Clauses);
 
@@ -2235,16 +2184,11 @@ type_check_fun(Env, Clauses) ->
     %% accurate type to the whole expression.
     %% TODO: Modify OTP's type syntax to allow returning an intersection type.
     {RetTy, _VB} = infer_clauses(Env, Clauses),
-    FunTy = case RetTy of
-                {type, _, any, []} when not Env#env.infer ->
-                    type(any);
-                _SomeTypeToPropagate ->
-                    %% Create a fun type with the correct arity on the form
-                    %% fun((any(), any(), ...) -> RetTy).
-                    [{clause, _, Params, _Guards, _Body} | _] = Clauses,
-                    Arity = arity(length(Params)),
-                    create_fun_type(Arity, RetTy)
-            end,
+    %% Create a fun type with the correct arity on the form
+    %% fun((any(), any(), ...) -> RetTy).
+    [{clause, _, Params, _Guards, _Body} | _] = Clauses,
+    Arity = arity(length(Params)),
+    FunTy = create_fun_type(Arity, RetTy),
     %% Variable bindings inside the fun clauses are local inside the fun.
     {FunTy, Env}.
 
@@ -2559,7 +2503,7 @@ minimal_substitution(Cs, ResTy) ->
 -spec infer_arg_types([expr()], env()) -> [type()].
 infer_arg_types(Args, Env) ->
     lists:map(fun (Arg) ->
-                      {ArgTy, _VB} = type_check_expr(Env#env{infer = true}, Arg),
+                      {ArgTy, _VB} = type_check_expr(Env, Arg),
                       ArgTy
               end, Args).
 
@@ -2612,17 +2556,7 @@ compat_arith_type(Ty1, Ty2, Env) ->
 -spec type_check_comprehension(env(), _, expr(), _) -> {type(), env()}.
 type_check_comprehension(Env, lc, Expr, []) ->
     {Ty, _VB} = type_check_expr(Env, Expr),
-    RetTy = case Ty of
-                {type, _, any, []} when not Env#env.infer ->
-                    %% No type information to propagate. We don't infer a
-                    %% list type of the list comprehension when inference
-                    %% is disabled.
-                    type(any);
-                _ ->
-                    %% Propagate the type information
-                    {type, erl_anno:new(0), list, [Ty]}
-            end,
-    RetTy = ?assert_type(RetTy, type()),
+    RetTy = {type, erl_anno:new(0), list, [Ty]},
     {RetTy, Env};
 type_check_comprehension(Env, bc, Expr, []) ->
     {Ty, _VB} = type_check_expr(Env, Expr),
@@ -2795,7 +2729,7 @@ do_type_check_expr_in(Env, ResTy, {tuple, _, TS} = Tup) ->
         {elem_tys, Tyss} ->
             case type_check_tuple_union_in(Env, Tyss, TS) of
                 none ->
-                    {Ty, _VB} = type_check_expr(Env#env{infer = true}, Tup),
+                    {Ty, _VB} = type_check_expr(Env, Tup),
                     throw(type_error(Tup, Ty, ResTy));
                 VBs ->
                     union_var_binds(VBs, Env)
@@ -2804,7 +2738,7 @@ do_type_check_expr_in(Env, ResTy, {tuple, _, TS} = Tup) ->
             {_Tys, VBs} = lists:unzip([type_check_expr(Env, Expr) || Expr <- TS ]),
             union_var_binds(VBs, Env);
         {type_error, _} ->
-            {Ty, _VB} = type_check_expr(Env#env{infer = true}, Tup),
+            {Ty, _VB} = type_check_expr(Env, Tup),
             throw(type_error(Tup, Ty, ResTy))
     end;
 
@@ -2958,8 +2892,6 @@ do_type_check_expr_in(Env, Ty, {'fun', _, {clauses, Clauses}} = Fun) ->
     end;
 do_type_check_expr_in(Env, ResTy, Expr = {'fun', P, {function, Name, Arity}}) ->
     case get_bounded_fun_type_list(Name, Arity, Env, P) of
-        [?type(any)] when not Env#env.infer ->
-            Env;
         [?type(any)] ->
             FunType = create_fun_type(Arity, type(any)),
             case subtype(FunType, ResTy, Env) of
@@ -3259,7 +3191,7 @@ type_check_logic_op_in(Env, ResTy, {op, _, Op, Arg1, Arg2} = OrigExpr) when Op =
             VarBinds2 = type_check_expr_in(EnvArg2, ResTy, Arg2),
             union_var_binds(VarBinds1, VarBinds2, Env);
         false ->
-            {Arg2Ty, _VB} = type_check_expr(Env#env{infer = true}, Arg2),
+            {Arg2Ty, _VB} = type_check_expr(Env, Arg2),
             Ty = type(union, [Arg2Ty, Target]),
             throw(type_error(OrigExpr, Ty, ResTy))
     end;
@@ -3500,8 +3432,8 @@ type_check_comprehension_in(Env, ResTy, OrigExpr, Compr, Expr, P, [Pred | Quals]
 -spec type_check_assocs(env(), _) -> {[type()], env()}.
 type_check_assocs(Env, [{Assoc, _P, Key, Val}| Assocs])
   when Assoc == map_field_assoc orelse Assoc == map_field_exact ->
-    {KeyTy, _KeyVB} = type_check_expr(Env#env{infer = true}, Key),
-    {ValTy, _ValVB} = type_check_expr(Env#env{infer = true}, Val),
+    {KeyTy, _KeyVB} = type_check_expr(Env, Key),
+    {ValTy, _ValVB} = type_check_expr(Env, Val),
     {AssocTys, VB}   = type_check_assocs(Env, Assocs),
     {[type(Assoc, [KeyTy, ValTy]) | AssocTys], VB};
 type_check_assocs(Env, []) ->
@@ -5829,7 +5761,6 @@ create_env(#parsedata{module    = Module
          tenv = TEnv,
          imported = Imported,
          %% Store some type checking options in the environment
-         infer = proplists:get_bool(infer, Opts),
          verbose = proplists:get_bool(verbose, Opts),
          union_size_limit = proplists:get_value(union_size_limit, Opts,
                                                 default_union_size_limit()),

src/typechecker.hrl

@@ -10,7 +10,6 @@
               imported          = #{}           :: #{{atom(), arity()} => module()},
               venv              = #{}           :: typechecker:venv(),
               tenv                              :: gradualizer_lib:tenv(),
-              infer             = false         :: boolean(),
               verbose           = false         :: boolean(),
               exhaust           = true          :: boolean(),
               %% Controls driving the type checking algorithm

test/gradualizer_cli_tests.erl

@@ -7,7 +7,7 @@
 help_test() ->
     ?assertEqual(help, gradualizer_cli:handle_args([])),
     ?assertEqual(help, gradualizer_cli:handle_args(["--help"])),
-    ?assertEqual(help, gradualizer_cli:handle_args(["--infer", "-h", "other.junk"])).
+    ?assertEqual(help, gradualizer_cli:handle_args(["-h", "other.junk"])).
 
 help_output_no_halt_test() ->
     %% This gives code coverage to the printing of the help text.
@@ -18,19 +18,12 @@ version_test() ->
 
 no_file_test() ->
     ?assertMatch({error, "No files"++_},
-                 gradualizer_cli:handle_args(["--infer"])).
+                 gradualizer_cli:handle_args(["--solve_constraints"])).
 
 invalid_arg_test() ->
     ?assertMatch({error, "Unknown"++_},
                  gradualizer_cli:handle_args(["--invalid-arg", "file.erl"])).
 
-infer_test() ->
-    {ok, _Files, Opts} = gradualizer_cli:handle_args(["--infer", "--", "file.erl"]),
-    ?assert(proplists:get_bool(infer, Opts)).
-no_infer_test() ->
-    {ok, _Files, Opts} = gradualizer_cli:handle_args(["--no_infer", "file.erl"]),
-    ?assertNot(proplists:get_bool(infer, Opts)).
-
 verbose_test() ->
     {ok, _Files, Opts} = gradualizer_cli:handle_args(["--verbose", "file.erl"]),
     ?assert(proplists:get_bool(verbose, Opts)).

test/known_problems/should_fail/infer_any_pattern.erl

@@ -2,8 +2,6 @@
 
 -export([pat_any/1]).
 
--gradualizer([infer]).
-
 %% We would expect (at least when infer mode is enabled) that type of
 %% I, S and L is integer(), string() and list() respectively but
 %% currently they all become any()

test/known_problems/should_pass/binary_exhaustiveness_checking_should_pass.erl

@@ -1,7 +1,5 @@
 -module(binary_exhaustiveness_checking_should_pass).
 
--gradualizer([infer]).
-
 -export([f/0]).
 
 -spec f() -> ok.

test/should_fail/infer_enabled.erl

@@ -1,6 +1,5 @@
 -module(infer_enabled).
 
--gradualizer(infer).
 -export([f/0]).
 
 f() ->

test/should_fail/list_infer_fail.erl

@@ -1,6 +1,5 @@
 -module(list_infer_fail).
 
--gradualizer(infer).
 -export([f/0]).
 
 f() ->

test/should_fail/map_failing_expr.erl

@@ -1,5 +1,4 @@
 -module(map_failing_expr).
--gradualizer([infer]).
 
 -export([foo/0, bar/0]).
 

test/should_fail/named_fun_infer_fail.erl

@@ -1,6 +1,5 @@
 -module(named_fun_infer_fail).
 
--gradualizer(infer).
 -export([bar/0, sum/1]).
 
 -spec foo(integer()) -> integer().

test/should_pass/binary_exhaustiveness_checking.erl

@@ -1,7 +1,5 @@
 -module(binary_exhaustiveness_checking).
 
--gradualizer([infer]).
-
 -export([f/1, g/1, h/1, k/1, l/1]).
 
 f(<<>>) -> ok;

test/should_pass/list_infer_pass.erl

@@ -1,6 +1,5 @@
 -module(list_infer_pass).
 
--gradualizer(infer).
 -export([f/0]).
 
 f() ->

test/should_pass/map_infer_pass.erl

@@ -4,8 +4,6 @@
          kaboom1/0,
          kaboom2/0]).
 
--gradualizer([infer]).
-
 -spec not_good(#{good | bad := integer()}) -> integer().
 not_good(#{good := _}) -> 0;
 not_good(#{bad := _}) -> 1.

test/should_pass/named_fun_infer_pass.erl

@@ -1,6 +1,5 @@
 -module(named_fun_infer_pass).
 
--gradualizer(infer).
 -export([atom_sum/1]).
 
 %% Documents expected behaviour that the type of parameters are not inferred