Unify type_check_expr and type_check_expr_in

Makefile

@@ -133,8 +133,8 @@ test/arg.beam: test/should_fail/arg.erl
 .PHONY: build_test_data
 test_data_erls = $(wildcard test/known_problems/**/*.erl test/should_fail/*.erl test/should_pass/*.erl)
 build_test_data:
-	mkdir -p "test_data"
-	erlc $(TEST_ERLC_OPTS) -o test_data $(test_data_erls)
+	@mkdir -p "test_data"
+	@erlc $(TEST_ERLC_OPTS) -o test_data $(test_data_erls)
 
 EUNIT_OPTS =
 
@@ -150,24 +150,24 @@ eunit: compile-tests
 	 '$(erl_run_eunit), halt().'
 
 cli-tests: bin/gradualizer test/arg.beam
-	# CLI test cases
-	# 1. When checking a dir with erl files, erl file names are printed
-	bin/gradualizer test/dir \
+	@# CLI test cases
+	@# 1. When checking a dir with erl files, erl file names are printed
+	@bin/gradualizer test/dir \
 	2>&1|perl -0777 -ne 'm%^test/dir/test_in_dir.erl:% or die "CLI 1 ($$_)"'
-	# 2. When checking a beam file; beam file name is printed
-	bin/gradualizer test/arg.beam \
+	@# 2. When checking a beam file; beam file name is printed
+	@bin/gradualizer test/arg.beam \
 	2>&1|perl -0777 -ne 'm%^test/arg.beam:% or die "CLI 1 ($$_)"'
-	# 3. Brief formatting
-	bin/gradualizer --fmt_location brief test/dir \
+	@# 3. Brief formatting
+	@bin/gradualizer --fmt_location brief test/dir \
 	2>&1|perl -0777 -ne '/^test\/dir\/test_in_dir.erl:6:12: The variable/ or die "CLI 6 ($$_)"'
-	# 4. Verbose formatting
-	bin/gradualizer --fmt_location verbose --no_fancy test/dir \
+	@# 4. Verbose formatting
+	@bin/gradualizer --fmt_location verbose --no_fancy test/dir \
 	2>&1|perl -ne '/^test\/dir\/test_in_dir.erl: The variable N on line 6 at column 12/ or die "CLI 7 ($$_)"'
-	# 5. Possible to exclude prelude (-0777 from https://stackoverflow.com/a/30594643/497116)
-	bin/gradualizer --no_prelude test/should_pass/cyclic_otp_specs.erl \
+	@# 5. Possible to exclude prelude (-0777 from https://stackoverflow.com/a/30594643/497116)
+	@bin/gradualizer --no_prelude test/should_pass/cyclic_otp_specs.erl \
 	2>&1|perl -0777 -ne '/^test\/should_pass\/cyclic_otp_specs.erl: The type spec/g or die "CLI 9 ($$_)"'
 	# 6. Excluding prelude and then including it is a no-op
-	bin/gradualizer --no_prelude --specs_override_dir priv/prelude \
+	@bin/gradualizer --no_prelude --specs_override_dir priv/prelude \
 	  test/should_pass/cyclic_otp_specs.erl || (echo "CLI 10"; exit 1)
 
 # Cover compile, run eunit, export and generate reports
@@ -223,7 +223,7 @@ dialyze-tests: app $(DIALYZER_PLT)
 
 .PHONY: check_name_clashes
 check_name_clashes:
-	test/check_name_clashes.sh
+	@test/check_name_clashes.sh
 
 # DIALYZER_PLT is a variable understood directly by Dialyzer.
 # Exit status 2 = warnings were emitted

src/typechecker.erl

@@ -28,8 +28,9 @@
          minimal_substitution/2,
          type_vars_variances/1]).
 
--compile([warn_missing_spec, warn_missing_spec_all,
-          warnings_as_errors]).
+-compile([warn_missing_spec, warn_missing_spec_all]).
+%,
+          %warnings_as_errors]).
 
 -include("typelib.hrl").
 
@@ -1861,12 +1862,15 @@ do_type_check_expr(Env, {match, _, Pat, Expr}) ->
                                 _Other -> UBoundNorm end,
     {UBound, Env2};
 do_type_check_expr(Env, {'if', _, Clauses}) ->
-    infer_clauses(Env, Clauses);
+    {Ty, Env1} = infer_clauses(Env, Clauses),
+    _Env2 = check_clauses(Env, [], Ty, Clauses, capture_vars),
+    {Ty, Env1};
 do_type_check_expr(Env, {'case', _, Expr, Clauses}) ->
-    {_ExprTy, Env1} = type_check_expr(Env, Expr),
+    {ExprTy, Env1} = type_check_expr(Env, Expr),
     Env2 = add_var_binds(Env, Env1, Env),
-    {Ty, VB} = infer_clauses(Env2, Clauses),
-    {Ty, union_var_binds(Env1, VB, Env)};
+    {Ty, Env3} = infer_clauses(Env2, Clauses),
+    _Env4 = check_clauses(Env2, [ExprTy], Ty, Clauses, capture_vars),
+    {Ty, union_var_binds(Env1, Env3, Env)};
 do_type_check_expr(Env, {tuple, _, TS}) ->
     {Tys, VarBindsList} = lists:unzip([ type_check_expr(Env, Expr) || Expr <- TS ]),
     InferredTy = type(tuple, Tys),
@@ -2634,11 +2638,28 @@ type_check_comprehension(Env, Compr, Expr, [Guard | Quals]) ->
       ResTy :: type(),
       Expr :: expr().
 type_check_expr_in(Env, ResTy, Expr) ->
+    {InferredTy, NewEnv} = type_check_expr(Env, Expr),
     ?verbose(Env, "~sChecking that ~ts :: ~ts~n",
-            [gradualizer_fmt:format_location(Expr, brief), erl_prettypr:format(Expr), typelib:pp_type(ResTy)]),
-    NormResTy = normalize(ResTy, Env),
-    R = ?throw_orig_type(do_type_check_expr_in(Env, NormResTy, Expr), ResTy, NormResTy),
-    ?assert_type(R, env()).
+            [gradualizer_fmt:format_location(Expr, brief),
+             erl_prettypr:format(Expr),
+             typelib:pp_type(ResTy)]),
+    case subtype(InferredTy, ResTy, NewEnv) of
+        true ->
+            NewEnv;
+        false ->
+            throw(type_error(Expr, InferredTy, ResTy))
+    end.
+
+%-spec type_check_expr_in(Env, ResTy, Expr) -> Env when
+%      Env :: env(),
+%      ResTy :: type(),
+%      Expr :: expr().
+%type_check_expr_in(Env, ResTy, Expr) ->
+%    ?verbose(Env, "~sChecking that ~ts :: ~ts~n",
+%            [gradualizer_fmt:format_location(Expr, brief), erl_prettypr:format(Expr), typelib:pp_type(ResTy)]),
+%    NormResTy = normalize(ResTy, Env),
+%    R = ?throw_orig_type(do_type_check_expr_in(Env, NormResTy, Expr), ResTy, NormResTy),
+%    ?assert_type(R, env()).
 
 -spec do_type_check_expr_in(Env, ResTy, Expr) -> Env when
       Env :: env(),

test/known_problems/should_fail/arith_op.erl

@@ -1,5 +1,14 @@
 -module(arith_op).
--export([int_error/2]).
+
+-export([failplus/1,
+         faildivvar/1,
+         int_error/2]).
+
+-spec failplus(_) -> tuple().
+failplus(X) -> X + X.
+
+-spec faildivvar(_) -> boolean().
+faildivvar(X) -> X div X.
 
 -spec int_error(any(), float()) -> integer().
 int_error(X, Y) ->

test/known_problems/should_fail/rel_op_should_fail.erl

@@ -0,0 +1,5 @@
+-module(rel_op_should_fail).
+-export([fail/1]).
+
+-spec fail(term()) -> tuple().
+fail(X) -> X > X.

test/known_problems/should_fail/return_fun_should_fail.erl

@@ -0,0 +1,8 @@
+-module(return_fun_should_fail).
+
+-export([return_fun_no_spec/0]).
+
+-spec return_fun_no_spec() -> integer().
+return_fun_no_spec() -> fun no_spec/0.
+
+no_spec() -> ok.

test/known_problems/should_fail/rigid_type_variables_should_fail.erl

@@ -0,0 +1,6 @@
+-module(rigid_type_variables_should_fail).
+
+-export([bad_curry/1]).
+
+-spec bad_curry(fun(({A, B}) -> C)) -> fun((A, B) -> C).
+bad_curry(F) -> fun (X, _Y) -> F({X, X}) end.

test/should_pass/factorial.erl → test/known_problems/should_pass/factorial_should_pass.erl

@@ -1,9 +1,9 @@
--module(factorial).
+-module(factorial_should_pass).
 
 -export([factorial/1]).
 
 %% This tests multiple things:
-%%   * Type refinement of the argument. After the first clase,
+%%   * Type refinement of the argument. After the first clause,
 %%     we have N :: pos_integer().
 %%   * Multiplication is closed under pos_integer()
 %%   * pos_integer() - 1 :: non_neg_integer()

test/known_problems/should_pass/operator_subtypes_should_pass.erl

@@ -0,0 +1,72 @@
+-module(operator_subtypes_should_pass).
+
+-export([arith_op3/1,
+         arith_op4/1,
+         float_op2/2,
+         pos_op1/2,
+         nonneg_op1/2,
+         neg_op1/2,
+         word_op1/1,
+         word_op2/2,
+         word_op3/3,
+         list_op4/2,
+         list_op6/2,
+         list_op7/2,
+         list_op9/0,
+         unary_op3/1]).
+
+%% Arithmetic operations
+
+-spec arith_op3(non_neg_integer()) -> pos_integer().
+arith_op3(N) ->
+    id(N + 1).
+
+-spec arith_op4(non_neg_integer()) -> pos_integer().
+arith_op4(N) ->
+    id(1 + N).
+
+-spec id(pos_integer()) -> pos_integer().
+id(P) -> P.
+
+-spec float_op2(integer(), float()) -> float().
+float_op2(X, Y) -> X / Y.
+
+-spec pos_op1(pos_integer(), 1..10) -> pos_integer().
+pos_op1(X, Y) -> X * Y + 777 bor Y.
+
+-spec nonneg_op1(0..100, non_neg_integer()) -> non_neg_integer() | error.
+nonneg_op1(X, Y) -> X + Y * X div Y rem X band Y bor X bxor Y bsl X bsr Y.
+
+-spec neg_op1(neg_integer(), -10..-5 | -2..-1) -> neg_integer() | 0..10.
+neg_op1(X, Y) -> X + Y + (-10).
+
+-type word16() :: 0..65535.
+
+-spec word_op1(non_neg_integer()) -> word16().
+word_op1(N) -> N rem 65536.
+
+-spec word_op2(word16(), word16()) -> word16().
+word_op2(X, Y) -> X band Y bor 32768 bxor Y.
+
+-spec word_op3(word16(), non_neg_integer(), pos_integer()) -> word16().
+word_op3(X, Y, Z) -> (X bsr Y) div Z.
+
+%% List operations
+
+-spec list_op4([], [tuple()]) -> [].
+list_op4(Xs, Ys) -> Xs -- Ys.
+
+-spec list_op6([integer()], maybe_improper_list(integer(), tl)) -> maybe_improper_list(integer(), tl | 5).
+list_op6(Xs, Ys) -> Xs ++ Ys.
+
+-spec list_op7([integer(), ...], nonempty_improper_list(integer(), tl)) -> nonempty_improper_list(integer(), tl).
+list_op7(Xs, Ys) -> Xs ++ Ys.
+
+-spec list_op9() -> iolist().
+list_op9() ->
+    [$a | list_to_binary("b")].
+
+%% Unary operators
+
+-spec unary_op3(0..10) -> 1..11.
+unary_op3(X) -> - (bnot X).

test/should_pass/qlc_test.erl → test/known_problems/should_pass/qlc_test_should_pass.erl

@@ -1,4 +1,4 @@
--module(qlc_test).
+-module(qlc_test_should_pass).
 
 -export([test/0]).
 

test/known_problems/should_pass/record_refinement_should_pass.erl

@@ -0,0 +1,27 @@
+-module(record_refinement_should_pass).
+
+-export([refined_field/1,
+         refined_field_safe/1,
+         %refined_field_unsafe/1,
+         not_all_fields_refined/0]).
+
+-record(refined_field, {f :: integer() | undefined}).
+
+-spec refined_field(#refined_field{}) -> #refined_field{f :: integer()}.
+refined_field(#refined_field{f = undefined}) -> #refined_field{f = 0};
+refined_field(R) -> R.
+
+-spec refined_field_safe(#refined_field{f :: integer()}) -> #refined_field{f :: integer()}.
+refined_field_safe(#refined_field{f = I}) -> #refined_field{f = I + 1}.
+
+%% This doesn't fail, but calls refined_field_safe/1 which does,
+%% so we can't have it in tests/should_pass.
+-spec refined_field_unsafe(#refined_field{}) -> #refined_field{}.
+refined_field_unsafe(R = #refined_field{f = undefined}) -> R;
+refined_field_unsafe(R) -> refined_field_safe(R).
+
+-record(not_all_fields_refined_r, {a, b}).
+-type not_all_fields_refined_t() :: #not_all_fields_refined_r{b :: b | c}.
+
+-spec not_all_fields_refined() -> not_all_fields_refined_t().
+not_all_fields_refined() -> #not_all_fields_refined_r{b = c}.

test/known_problems/should_pass/refine_bound_var_on_mismatch.erl

@@ -2,16 +2,7 @@
 
 %% Note: Here we're refining an already bound variable
 
--export([refined_var_not_matching_itself/1,
-         refine_bound_var_by_pattern_mismatch/1]).
-
-%% Current error: Var is expected to have type y | z but has type x | y | z
--spec refined_var_not_matching_itself(x | y | z) -> ok.
-refined_var_not_matching_itself(Var) ->
-    case Var of
-        x   -> ok;
-        Var -> ok
-    end.
+-export([refine_bound_var_by_pattern_mismatch/1]).
 
 %% Current error: Var is expected to have type ok but it has type ok | nok
 -spec refine_bound_var_by_pattern_mismatch(ok | nok) -> ok.

test/known_problems/should_pass/refine_bound_var_should_pass.erl

@@ -0,0 +1,12 @@
+-module(refine_bound_var_should_pass).
+
+%% Note: Here we're refining an already bound variable
+
+-export([refined_var_not_matching_itself/1]).
+
+-spec refined_var_not_matching_itself(x | y | z) -> ok.
+refined_var_not_matching_itself(Var) ->
+    case Var of
+        x   -> ok;
+        Var -> ok
+    end.

test/known_problems/should_pass/refine_comparison_should_pass.erl

@@ -1,5 +1,7 @@
 -module(refine_comparison_should_pass).
 
+-gradualizer([no_skip_complex_guards]).
+
 -export([comp_map_value3/1]).
 
 -type my_map() :: #{value := integer() | nil}.

test/known_problems/should_pass/return_fun_should_pass.erl

@@ -0,0 +1,16 @@
+-module(return_fun_should_pass).
+
+-export([return_fun_intersection/0,
+        return_fun_union_intersection/0]).
+
+-spec return_fun_intersection() -> fun((any()) -> integer()).
+return_fun_intersection() -> fun number/1.
+
+-spec return_fun_union_intersection()
+                                   -> fun((atom()) -> atom()) |
+                                      fun((1..3) -> integer()).
+return_fun_union_intersection() -> fun number/1.
+
+-spec number(integer()) -> integer();
+            (float()) -> float().
+number(N) -> N.

test/should_fail/arith_op_fail.erl

@@ -1,15 +1,15 @@
 -module(arith_op_fail).
 
--export([failplus/1, faildivvar/1, faildivlit/1, failpositivedivision/1,
-         faildivprecise/1, failplusprecise/2, failminusprecisepos/2,
-         failminusnonneg/2, failminuspreciseneg/2,
-         failbnot/1, int_error/2, int_error2/2]).
-
--spec failplus(_) -> tuple().
-failplus(X) -> X + X.
-
--spec faildivvar(_) -> boolean().
-faildivvar(X) -> X div X.
+-export([faildivlit/1,
+         failpositivedivision/1,
+         faildivprecise/1,
+         failplusprecise/2,
+         failminusprecisepos/2,
+         failminusnonneg/2,
+         failminuspreciseneg/2,
+         failbnot/1,
+         int_error/2,
+         int_error2/2]).
 
 -spec faildivlit(boolean()) -> any() | boolean().
 faildivlit(X) -> X div 2.

test/known_problems/should_fail/binary_comprehension.erl → test/should_fail/binary_comprehension_fail.erl

@@ -1,4 +1,4 @@
--module(binary_comprehension).
+-module(binary_comprehension_fail).
 -compile([debug_info]).
 -export([
          bitstring_match/0