From f03817d6ba6ac14a5da0bda5d8053095f231e7f9 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 12:53:21 +0200
Subject: [PATCH 01/24] Add
 test/should_pass/spec_and_fun_clause_intersection_pass.erl

See https://github.com/josefs/Gradualizer/issues/410 for the example source.
---
 .../spec_and_fun_clause_intersection_pass.erl            | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test/should_pass/spec_and_fun_clause_intersection_pass.erl

diff --git a/test/should_pass/spec_and_fun_clause_intersection_pass.erl b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
new file mode 100644
index 00000000..e46cbfb5
--- /dev/null
+++ b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
@@ -0,0 +1,9 @@
+-module(spec_and_fun_clause_intersection_pass).
+
+-export([foo/1]).
+
+-spec foo(bar) -> bar;
+         (list()) -> baz | qux.
+foo(bar) -> bar;
+foo([]) -> baz;
+foo([a]) -> qux.

From ce055efe18f5ae3718552cf66dbf3664953b5f09 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 17:45:13 +0200
Subject: [PATCH 02/24] Add
 test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl

---
 .../spec_and_fun_clause_intersection_should_pass.erl   | 10 ++++++++++
 .../spec_and_fun_clause_intersection_pass.erl          |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl

diff --git a/test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl b/test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl
new file mode 100644
index 00000000..9f9b75bf
--- /dev/null
+++ b/test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl
@@ -0,0 +1,10 @@
+-module(spec_and_fun_clause_intersection_should_pass).
+
+-export([f/1]).
+
+-type t() :: {tag, any()}.
+
+-spec f(t()) -> string();
+       ([t()]) -> string().
+f(Types) when is_list(Types) -> lists:map(fun f/1, Types);
+f({tag, _}) -> "".
diff --git a/test/should_pass/spec_and_fun_clause_intersection_pass.erl b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
index e46cbfb5..e13553a1 100644
--- a/test/should_pass/spec_and_fun_clause_intersection_pass.erl
+++ b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
@@ -6,4 +6,4 @@
          (list()) -> baz | qux.
 foo(bar) -> bar;
 foo([]) -> baz;
-foo([a]) -> qux.
+foo([_|_]) -> qux.

From 927c7bc6c990ffe1b059625e8fdcd42ec91b7aac Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 19:07:16 +0200
Subject: [PATCH 03/24] Move
 test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl
 to should_pass

---
 .../spec_and_fun_clause_intersection_should_pass.erl   | 10 ----------
 .../spec_and_fun_clause_intersection_pass.erl          |  9 ++++++++-
 2 files changed, 8 insertions(+), 11 deletions(-)
 delete mode 100644 test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl

diff --git a/test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl b/test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl
deleted file mode 100644
index 9f9b75bf..00000000
--- a/test/known_problems/should_pass/spec_and_fun_clause_intersection_should_pass.erl
+++ /dev/null
@@ -1,10 +0,0 @@
--module(spec_and_fun_clause_intersection_should_pass).
-
--export([f/1]).
-
--type t() :: {tag, any()}.
-
--spec f(t()) -> string();
-       ([t()]) -> string().
-f(Types) when is_list(Types) -> lists:map(fun f/1, Types);
-f({tag, _}) -> "".
diff --git a/test/should_pass/spec_and_fun_clause_intersection_pass.erl b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
index e13553a1..65e403f1 100644
--- a/test/should_pass/spec_and_fun_clause_intersection_pass.erl
+++ b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
@@ -1,9 +1,16 @@
 -module(spec_and_fun_clause_intersection_pass).
 
--export([foo/1]).
+-export([foo/1, g/1]).
 
 -spec foo(bar) -> bar;
          (list()) -> baz | qux.
 foo(bar) -> bar;
 foo([]) -> baz;
 foo([_|_]) -> qux.
+
+-type t() :: {tag, any()}.
+
+-spec g(t()) -> string();
+       ([t()]) -> string().
+g(Types) when is_list(Types) -> lists:map(fun g/1, Types);
+g({tag, _}) -> "".

From d885a0c82da70d995aa7905775f8e6fa2220873a Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 21:06:37 +0200
Subject: [PATCH 04/24] Simplify fun_ty() and its handling

---
 src/typechecker.erl | 177 ++++++++++++++++----------------------------
 1 file changed, 64 insertions(+), 113 deletions(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index 296eec4d..9f440bed 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -1227,39 +1227,34 @@ allow_empty_list(Ty) ->
         false -> Ty
     end.
 
--type fun_ty() :: any
-		| {fun_ty, [type()], type(), constraints:constraints()}
-		| {fun_ty_any_args, type(), constraints:constraints()}
-		| {fun_ty_intersection, [fun_ty()], constraints:constraints()}
-		| {fun_ty_union, [fun_ty()], constraints:constraints()}
-		.
+-type fun_ty() :: {fun_ty, [type()], type(), constraints()}
+                | {fun_ty_intersection, [fun_ty()], constraints()}
+                | {fun_ty_union, [fun_ty()], constraints()}.
 
 %% Categorizes a function type.
 %% Normalizes the type (expand user-def and remote types). Errors for non-fun
 %% types are returned with the original non-normalized type.
 %% TODO: move tenv to back
--spec expect_fun_type(env(), type() | [type()]) -> fun_ty() | {type_error, type()}.
-expect_fun_type(Env, Type) ->
+-spec expect_fun_type(env(), type() | [type()], arity()) -> fun_ty() | {type_error, type()}.
+expect_fun_type(Env, Type, Arity) ->
     Normalized = case Type of
                      Types when is_list(Types) ->
                          [ normalize(Ty, Env) || Ty <- Types ];
                      Type ->
                          normalize(Type, Env)
                  end,
-    case expect_fun_type1(Env, Normalized) of
+    case expect_fun_type1(Env, Normalized, Arity) of
         type_error -> {type_error, Type};
         Other -> Other
     end.
 
 %% TODO: move tenv to back
--spec expect_fun_type1(env(), type() | [type()]) -> fun_ty() | type_error.
-expect_fun_type1(Env, BTy = {type, _, bounded_fun, [Ft, _Fc]}) ->
+-spec expect_fun_type1(env(), type() | [type()], arity()) -> fun_ty() | type_error.
+expect_fun_type1(Env, BTy = {type, _, bounded_fun, [Ft, _Fc]}, Arity) ->
     Sub = bounded_type_subst(Env, BTy),
-    case expect_fun_type1(Env, Ft) of
+    case expect_fun_type1(Env, Ft, Arity) of
         {fun_ty, ArgsTy, ResTy, Cs} ->
             {fun_ty, subst_ty(Sub, ArgsTy), subst_ty(Sub, ResTy), Cs};
-        {fun_ty_any_args, ResTy, Cs} ->
-            {fun_ty_any_args, subst_ty(Sub, ResTy), Cs};
         {fun_ty_intersection, Tys, Cs} ->
             {fun_ty_intersection, subst_ty(Sub, Tys), Cs};
         {fun_ty_union, Tys, Cs} ->
@@ -1267,18 +1262,21 @@ expect_fun_type1(Env, BTy = {type, _, bounded_fun, [Ft, _Fc]}) ->
         Err ->
             Err
     end;
-expect_fun_type1(_Env, {type, _, 'fun', [{type, _, product, ArgsTy}, ResTy]}) ->
+expect_fun_type1(_Env, {type, _, 'fun', [{type, _, product, ArgsTy}, ResTy]}, _Arity) ->
     {fun_ty, ArgsTy, ResTy, constraints:empty()};
-expect_fun_type1(_Env, {type, _, 'fun', []}) ->
-    any;
-expect_fun_type1(_Env, {type, _, 'fun', [{type, _, any}, ResTy]}) ->
+expect_fun_type1(_Env, {type, _, 'fun', []}, Arity) ->
+    ArgsTy = lists:duplicate(Arity, type(any)),
+    ResTy = type(any),
+    {fun_ty, ArgsTy, ResTy, constraints:empty()};
+expect_fun_type1(_Env, {type, _, 'fun', [{type, _, any}, ResTy]}, Arity) ->
+    ArgsTy = lists:duplicate(Arity, type(any)),
     %% We can assert the below,
     %% as we know Res2 is not {type, _, any}, which is explicitely matched on above.
     ResTy = ?assert_type(ResTy, type()),
-    {fun_ty_any_args, ResTy, constraints:empty()};
-expect_fun_type1(Env, Tys) when is_list(Tys) ->
+    {fun_ty, ArgsTy, ResTy, constraints:empty()};
+expect_fun_type1(Env, Tys, Arity) when is_list(Tys) ->
     %% This is a spec, not really a type().
-    case expect_intersection_type(Env, Tys) of
+    case expect_intersection_type(Env, Tys, Arity) of
         type_error ->
             type_error;
         [Ty] ->
@@ -1286,8 +1284,8 @@ expect_fun_type1(Env, Tys) when is_list(Tys) ->
         Tyss ->
             {fun_ty_intersection, Tyss, constraints:empty()}
     end;
-expect_fun_type1(Env, {type, _, union, UnionTys}) ->
-    case expect_fun_type_union(Env, UnionTys) of
+expect_fun_type1(Env, {type, _, union, UnionTys}, Arity) ->
+    case expect_fun_type_union(Env, UnionTys, Arity) of
         [] ->
             type_error;
         [Ty] ->
@@ -1295,29 +1293,32 @@ expect_fun_type1(Env, {type, _, union, UnionTys}) ->
         Tys ->
             {fun_ty_union, Tys, constraints:empty()}
     end;
-expect_fun_type1(_Env, {var, _, Var}) ->
+expect_fun_type1(_Env, {var, _, Var}, Arity) ->
+    ArgsTy = lists:duplicate(Arity, type(any)),
     ResTy = new_type_var(),
-    {fun_ty_any_args, {var, erl_anno:new(0), ResTy}
-    ,constraints:add_var(Var,
-       constraints:upper(ResTy,
-         {type, erl_anno:new(0), 'fun', [{type, erl_anno:new(0), any}
-                                        ,{var,  erl_anno:new(0), ResTy}]}))};
-expect_fun_type1(_Env, {type, _, any, []}) ->
-    any;
-expect_fun_type1(_Env, ?top()) ->
-    {fun_ty_any_args, top(), constraints:empty()};
-expect_fun_type1(_Env, _Ty) ->
+    ResTyUpper = {type, erl_anno:new(0), 'fun', [{type, erl_anno:new(0), any},
+                                                 {var,  erl_anno:new(0), ResTy}]},
+    {fun_ty, ArgsTy, {var, erl_anno:new(0), ResTy},
+     constraints:add_var(Var, constraints:upper(ResTy, ResTyUpper))};
+expect_fun_type1(_Env, {type, _, any, []}, Arity) ->
+    ArgsTy = lists:duplicate(Arity, type(any)),
+    ResTy = type(any),
+    {fun_ty, ArgsTy, ResTy, constraints:empty()};
+expect_fun_type1(_Env, ?top(), Arity) ->
+    ArgsTy = lists:duplicate(Arity, type(any)),
+    {fun_ty, ArgsTy, top(), constraints:empty()};
+expect_fun_type1(_Env, _Ty, _Arity) ->
     type_error.
 
--spec expect_intersection_type(env(), [tuple()]) -> [fun_ty()] | type_error.
-expect_intersection_type(_Env, []) ->
+-spec expect_intersection_type(env(), [tuple()], arity()) -> [fun_ty()] | type_error.
+expect_intersection_type(_Env, [], _Arity) ->
     [];
-expect_intersection_type(Env, [FunTy|Tys]) ->
-    case expect_fun_type1(Env, FunTy) of
+expect_intersection_type(Env, [FunTy|Tys], Arity) ->
+    case expect_fun_type1(Env, FunTy, Arity) of
         type_error ->
             type_error;
         Ty ->
-            case expect_intersection_type(Env, Tys) of
+            case expect_intersection_type(Env, Tys, Arity) of
                 type_error ->
                     type_error;
                 Tyss ->
@@ -1325,15 +1326,15 @@ expect_intersection_type(Env, [FunTy|Tys]) ->
             end
     end.
 
--spec expect_fun_type_union(env(), [tuple()]) -> [fun_ty()].
-expect_fun_type_union(_Env, []) ->
+-spec expect_fun_type_union(env(), [tuple()], arity()) -> [fun_ty()].
+expect_fun_type_union(_Env, [], _Arity) ->
     [];
-expect_fun_type_union(Env, [Ty|Tys]) ->
-    case expect_fun_type1(Env, Ty) of
+expect_fun_type_union(Env, [Ty|Tys], Arity) ->
+    case expect_fun_type1(Env, Ty, Arity) of
         type_error ->
-            expect_fun_type_union(Env, Tys);
+            expect_fun_type_union(Env, Tys, Arity);
         TyOut ->
-            [TyOut | expect_fun_type_union(Env, Tys)]
+            [TyOut | expect_fun_type_union(Env, Tys, Arity)]
     end.
 
 -spec expect_record_type(type(), atom(), env()) -> Any | FieldsTy | FieldsTys | TypeError when
@@ -1654,8 +1655,8 @@ do_type_check_expr(Env, {call, P, Name, Args}) ->
     Arity = length(Args),
     Arity = ?assert_type(Arity, arity()),
     {FunTy, VarBinds1, Cs1} = type_check_fun(Env, Name, Arity),
-    {ResTy, VarBinds2, Cs2} = type_check_call_ty(Env, expect_fun_type(Env, FunTy), Args
-                                                ,{Name, P, FunTy}),
+    {ResTy, VarBinds2, Cs2} = type_check_call_ty(Env, expect_fun_type(Env, FunTy, Arity),
+                                                 Args, {Name, P, FunTy}),
     {ResTy, union_var_binds(VarBinds1, VarBinds2, Env),
             constraints:combine(Cs1, Cs2)};
 
@@ -2123,24 +2124,6 @@ type_check_call_ty(Env, {fun_ty, ArgsTy, ResTy, Cs}, Args, E) ->
             LenArgs = ?assert_type(LenArgs, arity()),
             throw(argument_length_mismatch(P, LenTy, LenArgs))
     end;
-type_check_call_ty(Env, {fun_ty_any_args, ResTy, Cs}, Args, _E) ->
-    {_Tys, VarBindsList, Css} =
-        lists:unzip3(
-          [ type_check_expr(Env, Arg)
-            || Arg <- Args
-          ]),
-    {ResTy
-    ,union_var_binds(VarBindsList, Env)
-    ,constraints:combine([Cs | Css])};
-type_check_call_ty(Env, any, Args, _E) ->
-    {_Tys, VarBindsList, Css} =
-        lists:unzip3(
-          [ type_check_expr(Env, Arg)
-            || Arg <- Args
-          ]),
-    {type(any)
-    ,union_var_binds(VarBindsList, Env)
-    ,constraints:combine(Css)};
 type_check_call_ty(Env, {fun_ty_intersection, Tyss, Cs}, Args, E) ->
     {ResTy, VarBinds, CsI} = type_check_call_ty_intersect(Env, Tyss, Args, E),
     {ResTy, VarBinds, constraints:combine(Cs, CsI)};
@@ -2555,8 +2538,8 @@ do_type_check_expr_in(Env, ResTy, {call, _, {atom, _, record_info}, [_, _]} = Ca
 do_type_check_expr_in(Env, ResTy, {call, P, Name, Args} = OrigExpr) ->
     Arity = ?assert_type(length(Args), arity()),
     {FunTy, VarBinds, Cs} = type_check_fun(Env, Name, Arity),
-    {VarBinds2, Cs2} = type_check_call(Env, ResTy, OrigExpr, expect_fun_type(Env, FunTy), Args,
-                                       {P, Name, FunTy}),
+    {VarBinds2, Cs2} = type_check_call(Env, ResTy, OrigExpr, expect_fun_type(Env, FunTy, Arity),
+                                       Args, {P, Name, FunTy}),
     {union_var_binds(VarBinds, VarBinds2, Env), constraints:combine(Cs, Cs2)};
 do_type_check_expr_in(Env, ResTy, {lc, P, Expr, Qualifiers} = OrigExpr) ->
     type_check_comprehension_in(Env, ResTy, OrigExpr, lc, Expr, P, Qualifiers);
@@ -2565,15 +2548,10 @@ do_type_check_expr_in(Env, ResTy, {bc, P, Expr, Qualifiers} = OrigExpr) ->
 
 %% Functions
 do_type_check_expr_in(Env, Ty, {'fun', _, {clauses, Clauses}} = Fun) ->
-    case expect_fun_type(Env, Ty) of
-        any ->
-            {Env, constraints:empty()};
+    case expect_fun_type(Env, Ty, clause_arity(hd(Clauses))) of
         {fun_ty, ArgsTy, ResTy, Cs1} ->
             {Env1, Cs2} = check_clauses(Env, ArgsTy, ResTy, Clauses, bind_vars),
             {Env1, constraints:combine(Cs1, Cs2)};
-        {fun_ty_any_args, ResTy, Cs1} ->
-            {Env1, Cs2} = check_clauses(Env, any, ResTy, Clauses, bind_vars),
-            {Env1, constraints:combine(Cs1, Cs2)};
         %% TODO: Can this case actually happen?
         {fun_ty_intersection, Tyss, Cs1} ->
             {Env1, Cs2} = check_clauses_intersect(Env, Tyss, Clauses),
@@ -2621,15 +2599,10 @@ do_type_check_expr_in(Env, ResTy, Expr = {'fun', P, {function, M, F, A}}) ->
     end;
 do_type_check_expr_in(Env, Ty, {named_fun, _, FunName, Clauses} = Fun) ->
     Env1 = add_var_binds(Env#env{venv = #{ FunName => Ty }}, Env, Env),
-    case expect_fun_type(Env, Ty) of
-        any ->
-            {Env#env{venv = #{ FunName => Ty }}, constraints:empty()};
+    case expect_fun_type(Env, Ty, clause_arity(hd(Clauses))) of
         {fun_ty, ArgsTy, ResTy, Cs1} ->
             {Env2, Cs2} = check_clauses(Env1, ArgsTy, ResTy, Clauses, bind_vars),
             {Env2, constraints:combine(Cs1, Cs2)};
-        {fun_ty_any_args, ResTy, Cs1} ->
-            {Env2, Cs2} = check_clauses(Env1, any, ResTy, Clauses, bind_vars),
-            {Env2, constraints:combine(Cs1, Cs2)};
         %% TODO: Can this case actually happen?
         {fun_ty_intersection, Tyss, Cs1} ->
             {Env2, Cs2} = check_clauses_intersect(Env1, Tyss, Clauses),
@@ -3236,28 +3209,6 @@ type_check_call(Env, ResTy, OrigExpr, {fun_ty, ArgsTy, FunResTy, Cs}, Args, _) -
         false ->
             throw(type_error(OrigExpr, FunResTy, ResTy))
     end;
-type_check_call(Env, ResTy, OrigExpr, {fun_ty_any_args, FunResTy, Cs}, Args, _)  ->
-    {_Tys, VarBindsList, Css} =
-        lists:unzip3(
-          lists:map(fun (Arg) ->
-                            type_check_expr(Env, Arg)
-                    end, Args)
-         ),
-    case subtype(FunResTy, ResTy, Env) of
-        {true, Cs1} ->
-            { union_var_binds(VarBindsList, Env)
-            , constraints:combine([Cs, Cs1 | Css]) };
-        false ->
-            throw(type_error(OrigExpr, FunResTy, ResTy))
-    end;
-type_check_call(Env, _ResTy, _, any, Args, _E) ->
-    {_Tys, VarBindsList, Css} =
-        lists:unzip3(
-          lists:map(fun (Arg) ->
-                            type_check_expr(Env, Arg)
-                    end, Args)
-         ),
-    {union_var_binds(VarBindsList, Env), constraints:combine(Css)};
 type_check_call(Env, ResTy, OrigExpr, {fun_ty_intersection, Tys, Cs1}, Args, E) ->
     {VB, Cs2} = type_check_call_intersection(Env, ResTy, OrigExpr, Tys, Args, E),
     {VB, constraints:combine(Cs1, Cs2)};
@@ -3454,11 +3405,6 @@ check_clauses_union(Env, [Ty|Tys], Clauses) ->
 check_clauses_fun(Env, {fun_ty, ArgsTy, FunResTy, Cs1}, Clauses) ->
     {Env1, Cs2} = check_clauses(Env, ArgsTy, FunResTy, Clauses, bind_vars),
     {Env1, constraints:combine(Cs1, Cs2)};
-check_clauses_fun(Env, {fun_ty_any_args, FunResTy, Cs1}, Clauses) ->
-    {Env1, Cs2} = check_clauses(Env, any, FunResTy, Clauses, bind_vars),
-    {Env1, constraints:combine(Cs1, Cs2)};
-check_clauses_fun(Env, any, Clauses) ->
-    check_clauses(Env, any, type(any), Clauses, bind_vars);
 check_clauses_fun(Env, {fun_ty_intersection, Tys, Cs1}, Clauses) ->
     {Env1, Cs2} = check_clauses_intersect(Env, Tys, Clauses),
     {Env1, constraints:combine(Cs1, Cs2)};
@@ -3469,18 +3415,13 @@ check_clauses_fun(Env, {fun_ty_union, Tys, Cs1}, Clauses) ->
 %% Checks a list of clauses (if/case/fun/try/catch/receive).
 -spec check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) -> R when
       Env :: env(),
-      ArgsTy :: [type()] | any,
+      ArgsTy :: [type()],
       ResTy :: type(),
       Clauses :: [gradualizer_type:abstract_clause()],
       Caps :: capture_vars | bind_vars,
       R :: {env(), constraints:constraints()}.
-check_clauses(Env, any, ResTy, [{clause, _, Args, _, _} | _] = Clauses, Caps) ->
-    %% 'any' is the ... in the type fun((...) -> ResTy)
-    ArgsTy = lists:duplicate(length(Args), type(any)),
-    check_clauses(Env, ArgsTy, ResTy, Clauses, Caps);
 check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
-    %% This is fine, since we match on `any' in the clause above.
     ArgsTy = ?assert_type(ArgsTy, [type()]),
     %% Clauses for if, case, functions, receive, etc.
     {VarBindsList, Css, RefinedArgsTy, Env2} =
@@ -4163,11 +4104,21 @@ type_check_function(Env, {function, _, Name, NArgs, Clauses}) ->
         {ok, FunTy} ->
             NewEnv = Env#env{current_spec = FunTy},
             FunTyNoPos = [ typelib:remove_pos(Ty) || Ty <- FunTy ],
-            check_clauses_fun(NewEnv, expect_fun_type(NewEnv, FunTyNoPos), Clauses);
+            Arity = clause_arity(hd(Clauses)),
+            check_clauses_fun(NewEnv, expect_fun_type(NewEnv, FunTyNoPos, Arity), Clauses);
         error ->
             throw(internal_error(missing_type_spec, Name, NArgs))
     end.
 
+-spec clause_arity({clause, _, list(), _, _}) -> arity().
+clause_arity({clause, _, Args, _, _}) ->
+    arity(length(Args)).
+
+-spec arity(non_neg_integer()) -> arity().
+arity(I) ->
+    I < 256 orelse erlang:error(arity_overflow),
+    ?assert_type(I, arity()).
+
 -spec position_info_from_spec(form() | forms() | none) -> erl_anno:anno().
 position_info_from_spec(none) ->
     %% This simplifies testing internal functions.

From 4bca2cadcd7ab9bac1d8d2a763eff3b36e20d660 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 21:35:13 +0200
Subject: [PATCH 05/24] Handle arity() values more cleanly

---
 src/typechecker.erl | 31 +++++++++++++------------------
 1 file changed, 13 insertions(+), 18 deletions(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index 9f440bed..5471bed2 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -108,6 +108,7 @@
 -include("typechecker.hrl").
 -type env() :: #env{}.
 
+-include_lib("stdlib/include/assert.hrl").
 -include("gradualizer.hrl").
 
 -type constraints() :: constraints:constraints().
@@ -811,7 +812,7 @@ normalize_rec({user_type, _, Name, Args} = Type, Env) ->
             Type;
         not_found ->
             P = position_info_from_spec(Env#env.current_spec),
-            throw(undef(user_type, P, {Name, ?assert_type(length(Args), arity())}))
+            throw(undef(user_type, P, {Name, arity(length(Args))}))
     end;
 normalize_rec(T = ?top(), _Env) ->
     %% Don't normalize gradualizer:top().
@@ -828,9 +829,9 @@ normalize_rec({remote_type, _, [{atom, _, M}, {atom, _, N}, Args]}, Env) ->
             Ty = {user_type, 0, N, NormalizedArgs},
             typelib:annotate_user_type(M, ?assert_type(Ty, type()));
         not_exported ->
-            throw(not_exported(remote_type, P, {M, N, ?assert_type(length(Args), arity())}));
+            throw(not_exported(remote_type, P, {M, N, arity(length(Args))}));
         not_found ->
-            throw(undef(remote_type, P, {M, N, ?assert_type(length(Args), arity())}))
+            throw(undef(remote_type, P, {M, N, arity(length(Args))}))
     end;
 normalize_rec({op, _, _, _Arg} = Op, _Env) ->
     erl_eval:partial_eval(Op);
@@ -1652,8 +1653,7 @@ do_type_check_expr(Env, {call, _, {atom, _, record_info}, [_, _]} = Call) ->
     Ty = get_record_info_type(Call, Env),
     {Ty, Env, constraints:empty()};
 do_type_check_expr(Env, {call, P, Name, Args}) ->
-    Arity = length(Args),
-    Arity = ?assert_type(Arity, arity()),
+    Arity = arity(length(Args)),
     {FunTy, VarBinds1, Cs1} = type_check_fun(Env, Name, Arity),
     {ResTy, VarBinds2, Cs2} = type_check_call_ty(Env, expect_fun_type(Env, FunTy, Arity),
                                                  Args, {Name, P, FunTy}),
@@ -1793,7 +1793,7 @@ do_type_check_expr(Env, {named_fun, _, FunName, Clauses}) ->
                     %% Create a fun type of the correct arity
                     %% on the form fun((_,_,_) -> any()).
                     [{clause, _, Params, _Guards, _Block} | _] = Clauses,
-                    Arity = ?assert_type(length(Params), arity()),
+                    Arity = arity(length(Params)),
                     create_fun_type(Arity, type(any));
                 not Env#env.infer ->
                     type(any)
@@ -1919,8 +1919,7 @@ type_check_fun(Env, Clauses) ->
                     %% Create a fun type with the correct arity on the form
                     %% fun((any(), any(), ...) -> RetTy).
                     [{clause, _, Params, _Guards, _Body} | _] = Clauses,
-                    Arity = length(Params),
-                    Arity = ?assert_type(Arity, arity()),
+                    Arity = arity(length(Params)),
                     create_fun_type(Arity, RetTy)
             end,
     %% Variable bindings inside the fun clauses are local inside the fun.
@@ -2120,9 +2119,7 @@ type_check_call_ty(Env, {fun_ty, ArgsTy, ResTy, Cs}, Args, E) ->
             ,constraints:combine([Cs | Css])};
         {LenTy, LenArgs} ->
             P = element(2, E),
-            LenTy = ?assert_type(LenTy, arity()),
-            LenArgs = ?assert_type(LenArgs, arity()),
-            throw(argument_length_mismatch(P, LenTy, LenArgs))
+            throw(argument_length_mismatch(P, arity(LenTy), arity(LenArgs)))
     end;
 type_check_call_ty(Env, {fun_ty_intersection, Tyss, Cs}, Args, E) ->
     {ResTy, VarBinds, CsI} = type_check_call_ty_intersect(Env, Tyss, Args, E),
@@ -2536,7 +2533,7 @@ do_type_check_expr_in(Env, ResTy, {call, _, {atom, _, record_info}, [_, _]} = Ca
             throw(type_error(Call, ResTy, Ty))
     end;
 do_type_check_expr_in(Env, ResTy, {call, P, Name, Args} = OrigExpr) ->
-    Arity = ?assert_type(length(Args), arity()),
+    Arity = arity(length(Args)),
     {FunTy, VarBinds, Cs} = type_check_fun(Env, Name, Arity),
     {VarBinds2, Cs2} = type_check_call(Env, ResTy, OrigExpr, expect_fun_type(Env, FunTy, Arity),
                                        Args, {P, Name, FunTy}),
@@ -3192,8 +3189,8 @@ type_check_call_intersection_(Env, ResTy, OrigExpr, [Ty | Tys], Args, E) ->
 -spec type_check_call(env(), type(), _, _, _, _) -> {env(), constraints:constraints()}.
 type_check_call(_Env, _ResTy, _, {fun_ty, ArgsTy, _FunResTy, _Cs}, Args, {P, Name, _})
         when length(ArgsTy) /= length(Args) ->
-    LenTys = ?assert_type(length(ArgsTy), arity()),
-    LenArgs = ?assert_type(length(Args), arity()),
+    LenTys = arity(length(ArgsTy)),
+    LenArgs = arity(length(Args)),
     throw(type_error(call_arity, P, Name, LenTys, LenArgs));
 type_check_call(Env, ResTy, OrigExpr, {fun_ty, ArgsTy, FunResTy, Cs}, Args, _) ->
     {VarBindsList, Css} =
@@ -3528,9 +3525,7 @@ check_clause(Env, ArgsTy, ResTy, C = {clause, P, Args, Guards, Block}, Caps) ->
             ,union_var_binds([VarBinds1, VarBinds2, EnvNewest], EnvNewest)
             ,constraints:combine(Cs1, Cs2)};
         {LenTy, LenArgs} ->
-            LenTy = ?assert_type(LenTy, arity()),
-            LenArgs = ?assert_type(LenArgs, arity()),
-            throw(argument_length_mismatch(P, LenTy, LenArgs))
+            throw(argument_length_mismatch(P, arity(LenTy), arity(LenArgs)))
     end.
 %% DEBUG
 %check_clause(_Env, _ArgsTy, _ResTy, Term, _) ->
@@ -4116,7 +4111,7 @@ clause_arity({clause, _, Args, _, _}) ->
 
 -spec arity(non_neg_integer()) -> arity().
 arity(I) ->
-    I < 256 orelse erlang:error(arity_overflow),
+    ?assert(I < 256, arity_overflow),
     ?assert_type(I, arity()).
 
 -spec position_info_from_spec(form() | forms() | none) -> erl_anno:anno().

From 7a9c4bfa771109084d647e6f481af8be59ab1636 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 13:00:10 +0200
Subject: [PATCH 06/24] wip: Check function definition against its intersection
 spec/type

In other words, check all function clauses against all available spec clauses.
---
 src/gradualizer_fmt.erl |   3 +-
 src/typechecker.erl     | 107 ++++++++++++++++++++++++----------------
 2 files changed, 67 insertions(+), 43 deletions(-)

diff --git a/src/gradualizer_fmt.erl b/src/gradualizer_fmt.erl
index 7ca1dd91..d17522f9 100644
--- a/src/gradualizer_fmt.erl
+++ b/src/gradualizer_fmt.erl
@@ -149,7 +149,8 @@ format_type_error({argument_length_mismatch, Anno, LenTy, LenArgs}, Opts) ->
        format_location(Anno, verbose, Opts),
        LenTy,
        LenArgs]);
-format_type_error({type_error, unreachable_clause, Anno}, Opts) ->
+format_type_error({type_error, unreachable_clauses, Clauses}, Opts) ->
+    Anno = element(2, hd(Clauses)),
     io_lib:format(
       "~sThe clause~s cannot be reached~n",
       [format_location(Anno, brief, Opts),
diff --git a/src/typechecker.erl b/src/typechecker.erl
index 5471bed2..4b543e34 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -126,7 +126,7 @@
                     | no_type_match_intersection | non_number_argument_to_minus
                     | non_number_argument_to_plus | op_type_too_precise | operator_pattern | pattern
                     | receive_after | record_pattern | rel_error | relop | unary_error
-                    | unreachable_clause.
+                    | unreachable_clauses.
 -type undef() :: record | user_type | remote_type | record_field.
 
 -type error() :: {type_error, type_error()}
@@ -3369,31 +3369,6 @@ infer_clause(Env, {clause, _, Args, Guards, Block}) ->
     {Ty, VB, Cs} = type_check_block(EnvNew, Block),
     {Ty, union_var_binds(VB, EnvNew, EnvNew), Cs}.
 
--spec check_clauses_intersect(env(), [fun_ty()], Clauses) -> R when
-      Clauses :: [gradualizer_type:abstract_clause()],
-      R :: {env(), constraints()}.
-check_clauses_intersect(Env, [], _Clauses) ->
-    {Env, constraints:empty()};
-check_clauses_intersect(Env, [Ty|Tys], Clauses) ->
-    %% Variable bindings should not leak into subsequent clauses,
-    %% that's why we explicitely pass them as appropriate.
-    VEnv = Env#env.venv,
-    {Env1, Cs1} = check_clauses_fun(Env, Ty, Clauses),
-    {Env2, Cs2} = check_clauses_intersect(Env1#env{venv = VEnv}, Tys, Clauses),
-    {union_var_binds(Env1, Env2, Env), constraints:combine(Cs1, Cs2)}.
-
-check_clauses_union(_Env, [], _Clauses) ->
-    %% TODO: Improve quality of type error
-    throw(type_error(check_clauses));
-check_clauses_union(Env, [Ty|Tys], Clauses) ->
-    try
-        check_clauses_fun(Env, Ty, Clauses)
-    catch
-        Error when element(1,Error) == type_error ->
-            check_clauses_union(Env, Tys, Clauses)
-    end.
-
-
 -spec check_clauses_fun(Env, FunTy, Clauses) -> R when
       Env :: env(),
       FunTy :: _,
@@ -3409,35 +3384,85 @@ check_clauses_fun(Env, {fun_ty_union, Tys, Cs1}, Clauses) ->
     {Env1, Cs2} = check_clauses_union(Env, Tys, Clauses),
     {Env1, constraints:combine(Cs1, Cs2)}.
 
+-spec check_clauses_intersect(env(), [fun_ty()], Clauses) -> R when
+      Clauses :: [gradualizer_type:abstract_clause()],
+      R :: {env(), constraints()}.
+check_clauses_intersect(Env, Tys, Clauses) ->
+    %% TODO: don't drop the constraints!
+    {ArgsTyss, ResTys} =
+        lists:unzip(lists:map(fun ({fun_ty, ArgsTy, ResTy, _Cs1}) ->
+                                      {ArgsTy, ResTy}
+                              end, Tys)),
+    check_clauses(Env, {intersection, ArgsTyss}, {intersection, ResTys}, Clauses, bind_vars).
+
+check_clauses_union(_Env, [], _Clauses) ->
+    %% TODO: Improve quality of type error
+    throw(type_error(check_clauses));
+check_clauses_union(Env, [Ty|Tys], Clauses) ->
+    try
+        check_clauses_fun(Env, Ty, Clauses)
+    catch
+        Error when element(1,Error) == type_error ->
+            check_clauses_union(Env, Tys, Clauses)
+    end.
+
 %% Checks a list of clauses (if/case/fun/try/catch/receive).
 -spec check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) -> R when
       Env :: env(),
-      ArgsTy :: [type()],
-      ResTy :: type(),
+      ArgsTy :: [type()] | {intersection, [[type()]]},
+      ResTy :: type() | {intersection, [type()]},
       Clauses :: [gradualizer_type:abstract_clause()],
       Caps :: capture_vars | bind_vars,
       R :: {env(), constraints:constraints()}.
+check_clauses(Env, {intersection, [ArgsTys | ArgsTyss]}, {intersection, [ResTy | ResTys]}, Clauses, Caps) ->
+    Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
+    %Env1 = Env,
+    %% Clauses for if, case, functions, receive, etc.
+    try {check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTys, Env1, return), ArgsTyss, ResTys} of
+        {{remaining_clauses, RemainingClauses, _}, [], []} ->
+            throw(type_error(unreachable_clauses, RemainingClauses));
+        {{remaining_clauses, RemainingClauses, Env2}, [_|_], [_|_]} ->
+            %% Variable bindings should not leak into subsequent clauses,
+            %% that's why we explicitly pass them as appropriate.
+            VEnv = Env1#env.venv,
+            check_clauses(Env2#env{venv = VEnv}, {intersection, ArgsTyss}, {intersection, ResTys},
+                          RemainingClauses, Caps);
+        {Acc, _, _} ->
+            {VarBindsList, Css, _RefinedArgsTy, Env2} = Acc,
+            %% TODO: work in progress
+            %check_arg_exhaustiveness(Env2, ArgsTys, Clauses, RefinedArgsTy),
+            %Env3 = pop_clauses_controls(Env2),
+            Env3 = Env2,
+            {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}
+    catch
+        E ->
+            gradualizer_tracer:debug({?MODULE, ?LINE, E}),
+            throw(E)
+    end;
 check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
+    %% This is fine, since we handle the other option in the clause above.
     ArgsTy = ?assert_type(ArgsTy, [type()]),
     %% Clauses for if, case, functions, receive, etc.
     {VarBindsList, Css, RefinedArgsTy, Env2} =
-        lists:foldl(fun (Clause, {VBs, Css, RefinedArgsTy, EnvIn}) ->
-                            {NewRefinedArgsTy, Env2, Cs} =
-                                check_clause(EnvIn, RefinedArgsTy, ResTy, Clause, Caps),
-                            VB =
-                                refine_vars_by_mismatching_clause(Clause, EnvIn#env.venv, Env2),
-                            {[Env2 | VBs],
-                             [Cs | Css],
-                             NewRefinedArgsTy,
-                             Env2#env{venv = VB}}
-                    end,
-                    {[], [], ArgsTy, Env1},
-                    Clauses),
+        check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTy, Env1, throw),
     check_arg_exhaustiveness(Env2, ArgsTy, Clauses, RefinedArgsTy),
     Env3 = pop_clauses_controls(Env2),
     {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}.
 
+check_reachable_clauses(_ResTy, [], _Caps, VBs, Cs, RefinedArgsTy, Env, _) ->
+    {VBs, Cs, RefinedArgsTy, Env};
+check_reachable_clauses(_ResTy, Clauses, _Caps, _, _, [?type(none)|_], Env, Action) ->
+    case Action of
+        throw -> throw(type_error(unreachable_clauses, Clauses));
+        return -> {remaining_clauses, Clauses, Env}
+    end;
+check_reachable_clauses(ResTy, [Clause | Clauses], Caps, VBs, Css, RefinedArgsTy, EnvIn, Action) ->
+    {NewRefinedArgsTy, Env2, Cs} = check_clause(EnvIn, RefinedArgsTy, ResTy, Clause, Caps),
+    VB = refine_vars_by_mismatching_clause(Clause, EnvIn#env.venv, Env2),
+    check_reachable_clauses(ResTy, Clauses, Caps, [Env2 | VBs], [Cs | Css],
+                            NewRefinedArgsTy, Env2#env{venv = VB}, Action).
+
 push_clauses_controls(#env{} = Env, #clauses_controls{} = CC) ->
     ?verbose(Env, "Pushing ~p~n", [CC]),
     CStack = Env#env.clauses_stack,
@@ -3507,8 +3532,6 @@ some_type_not_none(Types) when is_list(Types) ->
 -spec check_clause(env(), [type()], type(), gradualizer_type:abstract_clause(),
 		   capture_vars | bind_vars) ->
         {RefinedTys :: [type()] , VarBinds :: env(), constraints:constraints()}.
-check_clause(_Env, [?type(none)|_], _ResTy, {clause, P, _Args, _Guards, _Block}, _) ->
-    throw(type_error(unreachable_clause, P));
 check_clause(Env, ArgsTy, ResTy, C = {clause, P, Args, Guards, Block}, Caps) ->
     ?verbose(Env, "~sChecking clause :: ~s~n", [gradualizer_fmt:format_location(C, brief), typelib:pp_type(ResTy)]),
     case {length(ArgsTy), length(Args)} of

From c42c44b57c66939d59f4d361eea6deb0dfebf9e3 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 23:31:55 +0200
Subject: [PATCH 07/24] Define lists:map/2 spec override preserving the input
 list (non)empty property

---
 priv/prelude/lists.specs.erl | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/priv/prelude/lists.specs.erl b/priv/prelude/lists.specs.erl
index 52b9795b..eb82e2c3 100644
--- a/priv/prelude/lists.specs.erl
+++ b/priv/prelude/lists.specs.erl
@@ -33,6 +33,10 @@
 -spec foldl(fun((T, Acc) -> Acc), Acc, [T]) -> Acc.
 -spec foldr(fun((T, Acc) -> Acc), Acc, [T]) -> Acc.
 
+%% Preserve the (non)empty property of the input list.
+-spec map(fun((A) -> B), [A, ...]) -> [B, ...];
+         (fun((A) -> B), [A]) -> [B].
+
 %% -spec mapfoldl(Fun, Acc0, List1) -> {List2, Acc1} when
 %%       Fun :: fun((A, AccIn) -> {B, AccOut}),
 %%       Acc0 :: term(),

From 43d3e3e391b540a7e9376d5e8b1d8ed4b9d12a32 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 23:40:03 +0200
Subject: [PATCH 08/24] Drop non-emptiness assertion in absform.erl

---
 src/absform.erl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/absform.erl b/src/absform.erl
index e4235bf0..1f32aaf4 100644
--- a/src/absform.erl
+++ b/src/absform.erl
@@ -32,7 +32,7 @@ normalize_record_field({typed_record_field,
 -spec normalize_function_type_list(FunTypeList) -> FunTypeList when
       FunTypeList :: gradualizer_type:af_function_type_list().
 normalize_function_type_list(FunTypeList) ->
-    ?assert_type(lists:map(fun normalize_function_type/1, FunTypeList), [B, ...]).
+    lists:map(fun normalize_function_type/1, FunTypeList).
 
 -spec normalize_function_type(BoundedFun | Fun) -> BoundedFun when
       BoundedFun :: gradualizer_type:af_constrained_function_type(),

From 9262a504655cd62e390de930c8d51b9f62285d74 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 24 Sep 2022 23:57:15 +0200
Subject: [PATCH 09/24] Add test/should_*/lists_map_nonempty_*.erl

---
 test/should_fail/lists_map_nonempty_fail.erl |  7 +++++++
 test/should_pass/lists_map_nonempty_pass.erl | 14 ++++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 test/should_fail/lists_map_nonempty_fail.erl
 create mode 100644 test/should_pass/lists_map_nonempty_pass.erl

diff --git a/test/should_fail/lists_map_nonempty_fail.erl b/test/should_fail/lists_map_nonempty_fail.erl
new file mode 100644
index 00000000..42c25436
--- /dev/null
+++ b/test/should_fail/lists_map_nonempty_fail.erl
@@ -0,0 +1,7 @@
+-module(lists_map_nonempty_fail).
+
+-export([f/1]).
+
+-spec f([A]) -> [A, ...].
+f(L) ->
+    lists:map(fun (El) -> El end, L).
diff --git a/test/should_pass/lists_map_nonempty_pass.erl b/test/should_pass/lists_map_nonempty_pass.erl
new file mode 100644
index 00000000..7bb4d625
--- /dev/null
+++ b/test/should_pass/lists_map_nonempty_pass.erl
@@ -0,0 +1,14 @@
+-module(lists_map_nonempty_pass).
+
+-export([f/1,
+         g/1]).
+
+-spec f([A, ...]) -> [A, ...].
+f(L) ->
+    lists:map(fun (El) -> El end, L).
+
+%% [A, ...] is a subtype of [A], so this is fine, too,
+%% even if lists:map/2 :: ((A) -> B, [A, ...]) -> [B, ...].
+-spec g([A, ...]) -> [A].
+g(L) ->
+    lists:map(fun (El) -> El end, L).

From 6266fea3934790feebd7870464ee64cc7a8ab019 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sun, 25 Sep 2022 10:25:10 +0200
Subject: [PATCH 10/24] Proceed with remaining spec clauses we don't match a
 spec clause

---
 src/typechecker.erl | 31 ++++++++++++++++++-------------
 1 file changed, 18 insertions(+), 13 deletions(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index 4b543e34..2576f571 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -3416,28 +3416,23 @@ check_clauses_union(Env, [Ty|Tys], Clauses) ->
       R :: {env(), constraints:constraints()}.
 check_clauses(Env, {intersection, [ArgsTys | ArgsTyss]}, {intersection, [ResTy | ResTys]}, Clauses, Caps) ->
     Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
-    %Env1 = Env,
     %% Clauses for if, case, functions, receive, etc.
-    try {check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTys, Env1, return), ArgsTyss, ResTys} of
+    case {check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTys, Env1, return), ArgsTyss, ResTys} of
         {{remaining_clauses, RemainingClauses, _}, [], []} ->
             throw(type_error(unreachable_clauses, RemainingClauses));
         {{remaining_clauses, RemainingClauses, Env2}, [_|_], [_|_]} ->
             %% Variable bindings should not leak into subsequent clauses,
             %% that's why we explicitly pass them as appropriate.
             VEnv = Env1#env.venv,
-            check_clauses(Env2#env{venv = VEnv}, {intersection, ArgsTyss}, {intersection, ResTys},
+            Env3 = pop_clauses_controls(Env2),
+            check_clauses(Env3#env{venv = VEnv}, {intersection, ArgsTyss}, {intersection, ResTys},
                           RemainingClauses, Caps);
         {Acc, _, _} ->
             {VarBindsList, Css, _RefinedArgsTy, Env2} = Acc,
             %% TODO: work in progress
             %check_arg_exhaustiveness(Env2, ArgsTys, Clauses, RefinedArgsTy),
-            %Env3 = pop_clauses_controls(Env2),
-            Env3 = Env2,
+            Env3 = pop_clauses_controls(Env2),
             {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}
-    catch
-        E ->
-            gradualizer_tracer:debug({?MODULE, ?LINE, E}),
-            throw(E)
     end;
 check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
@@ -3453,15 +3448,25 @@ check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
 check_reachable_clauses(_ResTy, [], _Caps, VBs, Cs, RefinedArgsTy, Env, _) ->
     {VBs, Cs, RefinedArgsTy, Env};
 check_reachable_clauses(_ResTy, Clauses, _Caps, _, _, [?type(none)|_], Env, Action) ->
+    %% We've exhausted this spec clause by matching the function clauses,
+    %% but there are still more function clauses to check.
     case Action of
         throw -> throw(type_error(unreachable_clauses, Clauses));
         return -> {remaining_clauses, Clauses, Env}
     end;
 check_reachable_clauses(ResTy, [Clause | Clauses], Caps, VBs, Css, RefinedArgsTy, EnvIn, Action) ->
-    {NewRefinedArgsTy, Env2, Cs} = check_clause(EnvIn, RefinedArgsTy, ResTy, Clause, Caps),
-    VB = refine_vars_by_mismatching_clause(Clause, EnvIn#env.venv, Env2),
-    check_reachable_clauses(ResTy, Clauses, Caps, [Env2 | VBs], [Cs | Css],
-                            NewRefinedArgsTy, Env2#env{venv = VB}, Action).
+    try check_clause(EnvIn, RefinedArgsTy, ResTy, Clause, Caps) of
+        {NewRefinedArgsTy, Env2, Cs} ->
+            VB = refine_vars_by_mismatching_clause(Clause, EnvIn#env.venv, Env2),
+            check_reachable_clauses(ResTy, Clauses, Caps, [Env2 | VBs], [Cs | Css],
+                                    NewRefinedArgsTy, Env2#env{venv = VB}, Action)
+    catch
+        E when element(1, E) =:= type_error andalso Action =:= return ->
+            %% We've not exhausted this spec clause, but we've got a type error,
+            %% e.g. a pattern in the function head doesn't match the spec.
+            %% We try with the remaining spec clauses.
+            {remaining_clauses, [Clause | Clauses], EnvIn}
+    end.
 
 push_clauses_controls(#env{} = Env, #clauses_controls{} = CC) ->
     ?verbose(Env, "Pushing ~p~n", [CC]),

From 3933cf1ddc3693db343e75cc28bdb60b5554cbf4 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sun, 25 Sep 2022 11:24:11 +0200
Subject: [PATCH 11/24] Add more tests to
 test/should_pass/spec_and_fun_clause_intersection_pass.erl

---
 .../spec_and_fun_clause_intersection_pass.erl | 35 ++++++++++++++-----
 1 file changed, 26 insertions(+), 9 deletions(-)

diff --git a/test/should_pass/spec_and_fun_clause_intersection_pass.erl b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
index 65e403f1..9fcde6c1 100644
--- a/test/should_pass/spec_and_fun_clause_intersection_pass.erl
+++ b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
@@ -1,16 +1,33 @@
 -module(spec_and_fun_clause_intersection_pass).
 
--export([foo/1, g/1]).
+-export([f/1, g/1, h/1, i/1]).
 
--spec foo(bar) -> bar;
-         (list()) -> baz | qux.
-foo(bar) -> bar;
-foo([]) -> baz;
-foo([_|_]) -> qux.
+-spec f(bar) -> bar;
+       (list()) -> baz | qux.
+f(bar) -> bar;
+f([]) -> baz;
+f([_|_]) -> qux.
 
 -type t() :: {tag, any()}.
 
--spec g(t()) -> string();
-       ([t()]) -> string().
-g(Types) when is_list(Types) -> lists:map(fun g/1, Types);
+%% Order of spec clauses matches the order of patterns in function clauses - this should pass.
+-spec g([t()]) -> string();
+       (t()) -> string().
+g([] = _Types) -> [];
+g([_|_] = Types) -> lists:map(fun g/1, Types);
 g({tag, _}) -> "".
+
+%% This wouldn't work if we took guards into account when matching clauses to specs.
+%% It only works because any pattern matches a var in `add_type_pat()'.
+%% It's a bit of a coincidence that it does - it might stop in the future,
+%% so let's deem it "non-official".
+-spec h(t()) -> string();
+       ([t()]) -> string().
+h(Types) when is_list(Types) -> lists:map(fun h/1, Types);
+h({tag, _}) -> "".
+
+%% Should this still warn about nonexhaustive patterns? Currently it doesn't.
+-spec i([t()]) -> string();
+       (t()) -> string().
+i([_|_] = Types) -> lists:map(fun i/1, Types);
+i({tag, _}) -> "".

From 72e3ef1c1703e9db95b740da15d352fd0b718b7d Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sun, 25 Sep 2022 11:25:13 +0200
Subject: [PATCH 12/24] Add
 test/should_fail/spec_and_fun_clause_intersection_fail.erl

---
 .../spec_and_fun_clause_intersection_fail.erl     | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test/should_fail/spec_and_fun_clause_intersection_fail.erl

diff --git a/test/should_fail/spec_and_fun_clause_intersection_fail.erl b/test/should_fail/spec_and_fun_clause_intersection_fail.erl
new file mode 100644
index 00000000..0dd99a14
--- /dev/null
+++ b/test/should_fail/spec_and_fun_clause_intersection_fail.erl
@@ -0,0 +1,15 @@
+-module(spec_and_fun_clause_intersection_fail).
+
+-export([g/1]).
+
+-type t() :: {tag, any()}.
+
+%% Order of spec clauses and function clauses does not match - should fail!
+%% Strictly speaking, this does not follow the official Erlang docs to the letter,
+%% but supporting out of order matching of function clauses vs spec clauses
+%% is an implementation nightmare.
+-spec g(t()) -> string();
+       ([t()]) -> string().
+g([] = _Types) -> [];
+g([_|_] = Types) -> lists:map(fun g/1, Types);
+g({tag, _}) -> "".

From 545a63d6c1c14bd6b2ae62c58b4c5f6232722c2d Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sun, 25 Sep 2022 14:09:03 +0200
Subject: [PATCH 13/24] Extend
 test/should_fail/spec_and_fun_clause_intersection_fail.erl with
 exhaustiveness checking test

---
 .../spec_and_fun_clause_intersection_fail.erl    | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/test/should_fail/spec_and_fun_clause_intersection_fail.erl b/test/should_fail/spec_and_fun_clause_intersection_fail.erl
index 0dd99a14..4dcb17ec 100644
--- a/test/should_fail/spec_and_fun_clause_intersection_fail.erl
+++ b/test/should_fail/spec_and_fun_clause_intersection_fail.erl
@@ -1,15 +1,21 @@
 -module(spec_and_fun_clause_intersection_fail).
 
--export([g/1]).
+-export([f/1, g/1]).
+
+-type t() :: {tag, integer()}.
 
--type t() :: {tag, any()}.
 
 %% Order of spec clauses and function clauses does not match - should fail!
 %% Strictly speaking, this does not follow the official Erlang docs to the letter,
 %% but supporting out of order matching of function clauses vs spec clauses
 %% is an implementation nightmare.
--spec g(t()) -> string();
+-spec f(t()) -> string();
        ([t()]) -> string().
-g([] = _Types) -> [];
-g([_|_] = Types) -> lists:map(fun g/1, Types);
+f([] = _Types) -> [];
+f([_|_] = Types) -> lists:map(fun f/1, Types);
+f({tag, _}) -> "".
+
+-spec g([t()]) -> string();
+       (t()) -> string().
+g([] = _Types) -> "";
 g({tag, _}) -> "".

From 0c54e64b11448fd959b084e3b8da425ef8da043f Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sun, 25 Sep 2022 14:17:11 +0200
Subject: [PATCH 14/24] Check exhaustiveness when checking function clauses
 against multiple spec clauses

---
 src/typechecker.erl | 32 ++++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index 2576f571..305177dc 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -3420,17 +3420,21 @@ check_clauses(Env, {intersection, [ArgsTys | ArgsTyss]}, {intersection, [ResTy |
     case {check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTys, Env1, return), ArgsTyss, ResTys} of
         {{remaining_clauses, RemainingClauses, _}, [], []} ->
             throw(type_error(unreachable_clauses, RemainingClauses));
-        {{remaining_clauses, RemainingClauses, Env2}, [_|_], [_|_]} ->
+        {{remaining_clauses, RemainingClauses, {RefinedArgsTys, Env2}}, [_|_], [_|_]} ->
             %% Variable bindings should not leak into subsequent clauses,
             %% that's why we explicitly pass them as appropriate.
             VEnv = Env1#env.venv,
+            %% Here we either switch to the next spec because of exhaustion of the current one
+            %% or we failed matching a function clause pattern to the spec clause.
+            %% In either case, we can check exhaustiveness of the spec clause up until now.
+            check_arg_exhaustiveness(Env2, ArgsTys, Clauses, RefinedArgsTys),
             Env3 = pop_clauses_controls(Env2),
             check_clauses(Env3#env{venv = VEnv}, {intersection, ArgsTyss}, {intersection, ResTys},
                           RemainingClauses, Caps);
         {Acc, _, _} ->
-            {VarBindsList, Css, _RefinedArgsTy, Env2} = Acc,
-            %% TODO: work in progress
-            %check_arg_exhaustiveness(Env2, ArgsTys, Clauses, RefinedArgsTy),
+            {VarBindsList, Css, RefinedArgsTys, Env2} = Acc,
+            %% We're done with all the function clauses.
+            check_arg_exhaustiveness(Env2, ArgsTys, Clauses, RefinedArgsTys),
             Env3 = pop_clauses_controls(Env2),
             {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}
     end;
@@ -3445,27 +3449,27 @@ check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env3 = pop_clauses_controls(Env2),
     {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}.
 
-check_reachable_clauses(_ResTy, [], _Caps, VBs, Cs, RefinedArgsTy, Env, _) ->
-    {VBs, Cs, RefinedArgsTy, Env};
-check_reachable_clauses(_ResTy, Clauses, _Caps, _, _, [?type(none)|_], Env, Action) ->
+check_reachable_clauses(_ResTy, [], _Caps, VBs, Cs, RefinedArgsTys, Env, _) ->
+    {VBs, Cs, RefinedArgsTys, Env};
+check_reachable_clauses(_ResTy, Clauses, _Caps, _, _, [?type(none)|_] = RefinedArgsTys, Env, Action) ->
     %% We've exhausted this spec clause by matching the function clauses,
     %% but there are still more function clauses to check.
     case Action of
         throw -> throw(type_error(unreachable_clauses, Clauses));
-        return -> {remaining_clauses, Clauses, Env}
+        return -> {remaining_clauses, Clauses, {RefinedArgsTys, Env}}
     end;
-check_reachable_clauses(ResTy, [Clause | Clauses], Caps, VBs, Css, RefinedArgsTy, EnvIn, Action) ->
-    try check_clause(EnvIn, RefinedArgsTy, ResTy, Clause, Caps) of
-        {NewRefinedArgsTy, Env2, Cs} ->
+check_reachable_clauses(ResTy, [Clause | Clauses], Caps, VBs, Css, RefinedArgsTys, EnvIn, Action) ->
+    try check_clause(EnvIn, RefinedArgsTys, ResTy, Clause, Caps) of
+        {NewRefinedArgsTys, Env2, Cs} ->
             VB = refine_vars_by_mismatching_clause(Clause, EnvIn#env.venv, Env2),
             check_reachable_clauses(ResTy, Clauses, Caps, [Env2 | VBs], [Cs | Css],
-                                    NewRefinedArgsTy, Env2#env{venv = VB}, Action)
+                                    NewRefinedArgsTys, Env2#env{venv = VB}, Action)
     catch
         E when element(1, E) =:= type_error andalso Action =:= return ->
             %% We've not exhausted this spec clause, but we've got a type error,
             %% e.g. a pattern in the function head doesn't match the spec.
-            %% We try with the remaining spec clauses.
-            {remaining_clauses, [Clause | Clauses], EnvIn}
+            %% We return to try with the remaining spec clauses.
+            {remaining_clauses, [Clause | Clauses], {RefinedArgsTys, EnvIn}}
     end.
 
 push_clauses_controls(#env{} = Env, #clauses_controls{} = CC) ->

From 767138c6e97bf142d318146be11cf83def770a5d Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sun, 25 Sep 2022 15:29:02 +0200
Subject: [PATCH 15/24] Add exhaustiveness checking examples to
 gradualizer_tracer

---
 src/gradualizer_tracer.erl | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/gradualizer_tracer.erl b/src/gradualizer_tracer.erl
index a52554ba..c580fc0a 100644
--- a/src/gradualizer_tracer.erl
+++ b/src/gradualizer_tracer.erl
@@ -105,6 +105,12 @@ start() ->
     %dbg:tpl(typechecker, refine_vars_by_mismatching_clause, x),
     %dbg:tpl(typechecker, check_arg_exhaustiveness, x),
 
+    %dbg:tpl(typechecker, check_arg_exhaustiveness, x),
+    %dbg:tpl(typechecker, exhaustiveness_checking, x),
+    %dbg:tpl(typechecker, all_refinable, x),
+    %dbg:tpl(typechecker, no_clause_has_guards, x),
+    %dbg:tpl(typechecker, some_type_not_none, x),
+
     %dbg:tpl(typechecker, check_clause, x),
     %dbg:tpl(typechecker, check_clause, x),
     %dbg:tpl(typechecker, add_types_pats, x),

From 54d16c0d8d5ca0ec5888abe798f5f78753c634cb Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sun, 25 Sep 2022 16:52:21 +0200
Subject: [PATCH 16/24] Properly self-check remove_pos/1 using the new function
 intersection typing machinery

---
 src/gradualizer_type.erl |  6 ++++--
 src/typechecker.erl      |  2 +-
 src/typelib.erl          | 43 ++++++++++++++++++++++++++--------------
 3 files changed, 33 insertions(+), 18 deletions(-)

diff --git a/src/gradualizer_type.erl b/src/gradualizer_type.erl
index c3a1767d..7af0568c 100644
--- a/src/gradualizer_type.erl
+++ b/src/gradualizer_type.erl
@@ -22,12 +22,14 @@
 %% Export the additional types that gradualizer uses
 -export_type([abstract_pattern/0,
               af_assoc_type/0,
+              af_binary_op/1,
               af_constrained_function_type/0,
               af_constraint/0,
               af_fun_type/0,
               af_function_type_list/0,
               af_record_field/1,
               af_string/0,
+              af_unary_op/1,
               binary_op/0,
               gr_type_var/0,
               unary_op/0]).
@@ -213,6 +215,7 @@
                        | af_bitstring_type()
                        | af_empty_list_type()
                        | af_fun_type()
+                       | af_constrained_function_type()
                        | af_integer_range_type()
                        | af_map_type()
                        | af_predefined_type()
@@ -237,8 +240,7 @@
 -type af_fun_type() :: {'type', anno(), 'fun', []}
                      | {'type', anno(), 'fun', [{'type', anno(), 'any'} |
                                                 abstract_type()]}
-                     | af_function_type()
-                     | af_constrained_function_type().
+                     | af_function_type().
 
 -type af_integer_range_type() ::
         {'type', anno(), 'range', [af_singleton_integer_type()]}.
diff --git a/src/typechecker.erl b/src/typechecker.erl
index 305177dc..2844f0f9 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -4130,7 +4130,7 @@ type_check_function(Env, {function, _, Name, NArgs, Clauses}) ->
     case maps:find({Name, NArgs}, Env#env.fenv) of
         {ok, FunTy} ->
             NewEnv = Env#env{current_spec = FunTy},
-            FunTyNoPos = [ typelib:remove_pos(Ty) || Ty <- FunTy ],
+            FunTyNoPos = [ typelib:remove_pos(?assert_type(Ty, type())) || Ty <- FunTy ],
             Arity = clause_arity(hd(Clauses)),
             check_clauses_fun(NewEnv, expect_fun_type(NewEnv, FunTyNoPos, Arity), Clauses);
         error ->
diff --git a/src/typelib.erl b/src/typelib.erl
index f207e9f6..e8313afc 100644
--- a/src/typelib.erl
+++ b/src/typelib.erl
@@ -9,6 +9,7 @@
          reduce_type/3]).
 -export_type([constraint/0, function_type/0, extended_type/0]).
 
+-type af_constraint() :: gradualizer_type:af_constraint().
 -type type() :: gradualizer_type:abstract_type().
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -91,7 +92,28 @@ parse_type(Src) ->
 %% kept for user-defined types and record types. Filename is used to
 %% disambiguate between types with the same name from different modules.
 %% Annotated types as in Name :: Type are also removed.
--spec remove_pos(type()) -> type().
+-type any_t_no_args() :: {type, erl_anno:anno(), any}.
+-type unary_op() :: gradualizer_type:af_unary_op(_).
+-type binary_op() :: gradualizer_type:af_binary_op(_).
+
+-spec remove_pos(list()) -> list();
+                (any_t_no_args()) -> any_t_no_args();
+                (af_constraint()) -> af_constraint();
+                (type()) -> type();
+                (unary_op()) -> unary_op();
+                (binary_op()) -> binary_op().
+remove_pos([]) ->
+    [];
+remove_pos([_|_] = L) ->
+    lists:map(fun remove_pos/1, L);
+remove_pos({type, _, any}) ->
+    %% special case for `fun((...) -> R)`,
+    %% the only place where `{type, _, any}` can occur
+    {type, erl_anno:new(0), any};
+remove_pos({type, _, constraint, [{atom, _, is_subtype}, Args]}) ->
+    Args = ?assert_type(Args, [type()]),
+    L = erl_anno:new(0),
+    {type, L, constraint, [{atom, L, is_subtype}, lists:map(fun remove_pos/1, Args)]};
 remove_pos({Type, _, Value})
   when Type == atom; Type == integer; Type == char; Type == var ->
     {Type, erl_anno:new(0), Value};
@@ -103,30 +125,21 @@ remove_pos({type, Anno, record, [Name | TypedFields]}) ->
      [remove_pos(Name)] ++ lists:map(fun remove_pos/1, TypedFields)};
 remove_pos({type, _, field_type, [FName, FTy]}) ->
     {type, erl_anno:new(0), field_type, [remove_pos(FName), remove_pos(FTy)]};
-remove_pos({type, _, bounded_fun, [FT, Cs]}) ->
-    {type, erl_anno:new(0), bounded_fun, [remove_pos(FT)
-                                         ,lists:map(fun remove_pos/1, Cs)]};
-remove_pos({type, _, constraint, [{atom, _, is_subtype}, [V, T]]}) ->
-    {type, erl_anno:new(0), constraint, [{atom, erl_anno:new(0), is_subtype}
-                                        ,[remove_pos(V), remove_pos(T)]]};
-remove_pos({type, _, 'fun', [{type, _, any}, RetTy]}) ->
-    %% special case for `fun((...) -> R)`,
-    %% the only place where `{type, _, any}` can occur
-    {type, erl_anno:new(0), 'fun', [{type, erl_anno:new(0), any}
-                                   ,remove_pos(RetTy)]};
 remove_pos({type, _, Type, Params}) when is_list(Params) ->
     {type, erl_anno:new(0), Type, lists:map(fun remove_pos/1, Params)};
 remove_pos({type, _, Type, any}) when Type == tuple; Type == map ->
     {type, erl_anno:new(0), Type, any};
-remove_pos({type, _, Assoc, Tys}) when Assoc == map_field_exact;
-				      Assoc == map_field_assoc ->
+remove_pos({type, _, Assoc, Tys})
+  when Assoc == map_field_exact;
+       Assoc == map_field_assoc ->
     {type, erl_anno:new(0), Assoc, lists:map(fun remove_pos/1, Tys)};
 remove_pos({remote_type, _, [Mod, Name, Params]}) ->
+    Params = ?assert_type(Params, list()),
     Params1 = lists:map(fun remove_pos/1, Params),
     {remote_type, erl_anno:new(0), [Mod, Name, Params1]};
 remove_pos({ann_type, _, [_Var, Type]}) ->
     %% Also remove annotated types one the form Name :: Type
-    remove_pos(Type);
+    remove_pos(?assert_type(Type, type()));
 remove_pos({op, _, Op, Type}) ->
     {op, erl_anno:new(0), Op, remove_pos(Type)};
 remove_pos({op, _, Op, Type1, Type2}) ->

From c887f86f082b895109cef79838a352aefa80c71c Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Wed, 28 Sep 2022 00:56:41 +0200
Subject: [PATCH 17/24] Do not require spec and fun clause order to match

This is achieved by cycling over fun clauses for each spec clause.
---
 src/typechecker.erl                           | 110 ++++++++++++------
 .../spec_and_fun_clause_intersection_fail.erl |  19 ++-
 .../spec_and_fun_clause_intersection_pass.erl |  30 +++--
 3 files changed, 102 insertions(+), 57 deletions(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index 2844f0f9..feb506c1 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -3372,7 +3372,7 @@ infer_clause(Env, {clause, _, Args, Guards, Block}) ->
 -spec check_clauses_fun(Env, FunTy, Clauses) -> R when
       Env :: env(),
       FunTy :: _,
-      Clauses :: [gradualizer_type:abstract_clause()],
+      Clauses :: [gradualizer_type:abstract_clause(), ...],
       R :: {env(), constraints:constraints()}.
 check_clauses_fun(Env, {fun_ty, ArgsTy, FunResTy, Cs1}, Clauses) ->
     {Env1, Cs2} = check_clauses(Env, ArgsTy, FunResTy, Clauses, bind_vars),
@@ -3385,15 +3385,17 @@ check_clauses_fun(Env, {fun_ty_union, Tys, Cs1}, Clauses) ->
     {Env1, constraints:combine(Cs1, Cs2)}.
 
 -spec check_clauses_intersect(env(), [fun_ty()], Clauses) -> R when
-      Clauses :: [gradualizer_type:abstract_clause()],
+      Clauses :: [gradualizer_type:abstract_clause(), ...],
       R :: {env(), constraints()}.
 check_clauses_intersect(Env, Tys, Clauses) ->
     %% TODO: don't drop the constraints!
-    {ArgsTyss, ResTys} =
-        lists:unzip(lists:map(fun ({fun_ty, ArgsTy, ResTy, _Cs1}) ->
-                                      {ArgsTy, ResTy}
-                              end, Tys)),
-    check_clauses(Env, {intersection, ArgsTyss}, {intersection, ResTys}, Clauses, bind_vars).
+    FunTys = lists:map(fun ({fun_ty, ArgsTys, ResTy, _Cs1}) ->
+                               {ArgsTys, ResTy}
+                       end, Tys),
+    RefinedArgsTyss = maps:from_list(lists:map(fun ({ArgsTys, _}) ->
+                                                       {ArgsTys, ArgsTys}
+                                               end, FunTys)),
+    check_clauses(Env, {intersection, FunTys}, {Clauses, #{}, RefinedArgsTyss}, Clauses, bind_vars).
 
 check_clauses_union(_Env, [], _Clauses) ->
     %% TODO: Improve quality of type error
@@ -3409,34 +3411,57 @@ check_clauses_union(Env, [Ty|Tys], Clauses) ->
 %% Checks a list of clauses (if/case/fun/try/catch/receive).
 -spec check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) -> R when
       Env :: env(),
-      ArgsTy :: [type()] | {intersection, [[type()]]},
-      ResTy :: type() | {intersection, [type()]},
-      Clauses :: [gradualizer_type:abstract_clause()],
+      ArgsTy :: [type()] | {intersection, [{[type()], type()}]},
+      ResTy :: type() | {{intersection, [{[type()], type()}]}, #{}},
+      Clauses :: [gradualizer_type:abstract_clause(), ...],
       Caps :: capture_vars | bind_vars,
       R :: {env(), constraints:constraints()}.
-check_clauses(Env, {intersection, [ArgsTys | ArgsTyss]}, {intersection, [ResTy | ResTys]}, Clauses, Caps) ->
-    Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
-    %% Clauses for if, case, functions, receive, etc.
-    case {check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTys, Env1, return), ArgsTyss, ResTys} of
-        {{remaining_clauses, RemainingClauses, _}, [], []} ->
-            throw(type_error(unreachable_clauses, RemainingClauses));
-        {{remaining_clauses, RemainingClauses, {RefinedArgsTys, Env2}}, [_|_], [_|_]} ->
-            %% Variable bindings should not leak into subsequent clauses,
-            %% that's why we explicitly pass them as appropriate.
-            VEnv = Env1#env.venv,
-            %% Here we either switch to the next spec because of exhaustion of the current one
-            %% or we failed matching a function clause pattern to the spec clause.
-            %% In either case, we can check exhaustiveness of the spec clause up until now.
-            check_arg_exhaustiveness(Env2, ArgsTys, Clauses, RefinedArgsTys),
-            Env3 = pop_clauses_controls(Env2),
-            check_clauses(Env3#env{venv = VEnv}, {intersection, ArgsTyss}, {intersection, ResTys},
-                          RemainingClauses, Caps);
-        {Acc, _, _} ->
-            {VarBindsList, Css, RefinedArgsTys, Env2} = Acc,
-            %% We're done with all the function clauses.
-            check_arg_exhaustiveness(Env2, ArgsTys, Clauses, RefinedArgsTys),
-            Env3 = pop_clauses_controls(Env2),
-            {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}
+check_clauses(Env, {intersection, []}, _Acc, _Clauses, _Caps) ->
+    %% TODO: return the right constraints
+    {Env, constraints:empty()};
+check_clauses(Env, {intersection, [{ArgsTys, _ResTy} = FunTy | FunTys]},
+              {OrigClauses, Seen, RefinedArgsTyss},
+              [] = _Clauses, _Caps) ->
+    check_clauses(Env, {intersection, [FunTy | FunTys]},
+                  {OrigClauses, maps:put(ArgsTys, hd(OrigClauses), Seen), RefinedArgsTyss},
+                  OrigClauses, _Caps);
+check_clauses(Env, {intersection, [{ArgsTys, ResTy} = FunTy | FunTys]},
+              {OrigClauses, Seen, RefinedArgsTyss},
+              [Clause | Clauses], Caps) ->
+    MaybeRefinedArgsTys = maps:get(ArgsTys, RefinedArgsTyss),
+    case check_clauses_throw_if_already_seen(ArgsTys, MaybeRefinedArgsTys, Clause, Seen, Env) of
+        done ->
+            {Env, constraints:empty()};
+        {type_error, E} ->
+            throw(E);
+        ok ->
+
+            Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
+            %% Clauses for if, case, functions, receive, etc.
+
+            try check_clause(Env1, MaybeRefinedArgsTys, ResTy, Clause, Caps) of
+                {[?type(none) | _] = RefinedArgsTys, Env2, Cs} ->
+                    RefinedArgsTyss1 = maps:put(ArgsTys, RefinedArgsTys, RefinedArgsTyss),
+                    Seen1 = maps:put({ArgsTys, Clause}, true, Seen),
+                    check_clauses(Env1, {intersection, FunTys},
+                                  {OrigClauses, Seen1, RefinedArgsTyss1},
+                                  OrigClauses, Caps);
+                {RefinedArgsTys, Env2, Cs} ->
+                    RefinedArgsTyss1 = maps:put(ArgsTys, RefinedArgsTys, RefinedArgsTyss),
+                    Seen1 = maps:put({ArgsTys, Clause}, true, Seen),
+                    check_clauses(Env1, {intersection, [FunTy | FunTys]},
+                                  {OrigClauses, Seen1, RefinedArgsTyss1},
+                                  Clauses, Caps)
+            catch
+                E when element(1, E) =:= type_error ->
+                    %% We've not exhausted this spec clause, but we've got a type error,
+                    %% e.g. a pattern in the function head doesn't match the spec.
+                    Seen1 = maps:put({ArgsTys, Clause}, E, Seen),
+                    check_clauses(Env1, {intersection, [FunTy | FunTys]},
+                                  {OrigClauses, Seen1, RefinedArgsTyss},
+                                  Clauses, Caps)
+            end
+
     end;
 check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
@@ -3449,6 +3474,21 @@ check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env3 = pop_clauses_controls(Env2),
     {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}.
 
+check_clauses_throw_if_already_seen(ArgsTys, RefinedArgsTy, Clause, Seen, Env) ->
+    case maps:get({ArgsTys, Clause}, Seen, false) of
+        false ->
+            ok;
+        ok ->
+            done;
+        true ->
+            {clause, P, _, _, _} = Clause,
+            throw(nonexhaustive(P, gradualizer_lib:pick_values(RefinedArgsTy, Env)));
+        ClauseError ->
+            {type_error, ClauseError}
+    end.
+
+%% We return `{remaining_clauses, _, _, _, _}' either because of exhaustion of the current spec clause
+%% or because we failed matching a function clause pattern to the spec clause.
 check_reachable_clauses(_ResTy, [], _Caps, VBs, Cs, RefinedArgsTys, Env, _) ->
     {VBs, Cs, RefinedArgsTys, Env};
 check_reachable_clauses(_ResTy, Clauses, _Caps, _, _, [?type(none)|_] = RefinedArgsTys, Env, Action) ->
@@ -3456,7 +3496,7 @@ check_reachable_clauses(_ResTy, Clauses, _Caps, _, _, [?type(none)|_] = RefinedA
     %% but there are still more function clauses to check.
     case Action of
         throw -> throw(type_error(unreachable_clauses, Clauses));
-        return -> {remaining_clauses, Clauses, {RefinedArgsTys, Env}}
+        return -> {remaining_clauses, Clauses, RefinedArgsTys, Env, ok}
     end;
 check_reachable_clauses(ResTy, [Clause | Clauses], Caps, VBs, Css, RefinedArgsTys, EnvIn, Action) ->
     try check_clause(EnvIn, RefinedArgsTys, ResTy, Clause, Caps) of
@@ -3469,7 +3509,7 @@ check_reachable_clauses(ResTy, [Clause | Clauses], Caps, VBs, Css, RefinedArgsTy
             %% We've not exhausted this spec clause, but we've got a type error,
             %% e.g. a pattern in the function head doesn't match the spec.
             %% We return to try with the remaining spec clauses.
-            {remaining_clauses, [Clause | Clauses], {RefinedArgsTys, EnvIn}}
+            {remaining_clauses, [Clause | Clauses], RefinedArgsTys, EnvIn, E}
     end.
 
 push_clauses_controls(#env{} = Env, #clauses_controls{} = CC) ->
diff --git a/test/should_fail/spec_and_fun_clause_intersection_fail.erl b/test/should_fail/spec_and_fun_clause_intersection_fail.erl
index 4dcb17ec..bda38573 100644
--- a/test/should_fail/spec_and_fun_clause_intersection_fail.erl
+++ b/test/should_fail/spec_and_fun_clause_intersection_fail.erl
@@ -1,21 +1,20 @@
 -module(spec_and_fun_clause_intersection_fail).
 
--export([f/1, g/1]).
+-export([f/1, g/1, i/1]).
 
 -type t() :: {tag, integer()}.
 
-
-%% Order of spec clauses and function clauses does not match - should fail!
-%% Strictly speaking, this does not follow the official Erlang docs to the letter,
-%% but supporting out of order matching of function clauses vs spec clauses
-%% is an implementation nightmare.
--spec f(t()) -> string();
-       ([t()]) -> string().
-f([] = _Types) -> [];
-f([_|_] = Types) -> lists:map(fun f/1, Types);
+-spec f([t()]) -> string();
+       (t()) -> string().
+f(asd) -> "";
 f({tag, _}) -> "".
 
 -spec g([t()]) -> string();
        (t()) -> string().
 g([] = _Types) -> "";
 g({tag, _}) -> "".
+
+-spec i([t()]) -> string();
+       (t()) -> string().
+i([_|_] = Types) -> lists:map(fun i/1, Types);
+i({tag, _}) -> "".
diff --git a/test/should_pass/spec_and_fun_clause_intersection_pass.erl b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
index 9fcde6c1..c1c350f0 100644
--- a/test/should_pass/spec_and_fun_clause_intersection_pass.erl
+++ b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
@@ -1,6 +1,6 @@
 -module(spec_and_fun_clause_intersection_pass).
 
--export([f/1, g/1, h/1, i/1]).
+-export([f/1, g/1, g1/1, g2/1, h/1]).
 
 -spec f(bar) -> bar;
        (list()) -> baz | qux.
@@ -8,7 +8,7 @@ f(bar) -> bar;
 f([]) -> baz;
 f([_|_]) -> qux.
 
--type t() :: {tag, any()}.
+-type t() :: {tag, integer()}.
 
 %% Order of spec clauses matches the order of patterns in function clauses - this should pass.
 -spec g([t()]) -> string();
@@ -17,17 +17,23 @@ g([] = _Types) -> [];
 g([_|_] = Types) -> lists:map(fun g/1, Types);
 g({tag, _}) -> "".
 
-%% This wouldn't work if we took guards into account when matching clauses to specs.
-%% It only works because any pattern matches a var in `add_type_pat()'.
-%% It's a bit of a coincidence that it does - it might stop in the future,
-%% so let's deem it "non-official".
+%% Order of spec clauses doesn't match the order of patterns
+%% in function clauses - this should pass, too.
+-spec g1(t()) -> string();
+        ([t()]) -> string().
+g1([] = _Types) -> [];
+g1([_|_] = Types) -> lists:map(fun g1/1, Types);
+g1({tag, _}) -> "".
+
+%% Order of spec clauses doesn't match the order of patterns
+%% in function clauses and function clause patterns are mixed - will that pass?
+-spec g2(t()) -> string();
+        ([t()]) -> string().
+g2([] = _Types) -> [];
+g2({tag, _}) -> "";
+g2([_|_] = Types) -> lists:map(fun g2/1, Types).
+
 -spec h(t()) -> string();
        ([t()]) -> string().
 h(Types) when is_list(Types) -> lists:map(fun h/1, Types);
 h({tag, _}) -> "".
-
-%% Should this still warn about nonexhaustive patterns? Currently it doesn't.
--spec i([t()]) -> string();
-       (t()) -> string().
-i([_|_] = Types) -> lists:map(fun i/1, Types);
-i({tag, _}) -> "".

From 65befd80175d9f37407a361e0ed79c9283822149 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 15 Oct 2022 00:01:34 +0200
Subject: [PATCH 18/24] Fix regression: correctly use var binds from the
 previous clause

---
 src/typechecker.erl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index feb506c1..f2ef8eb1 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -3592,7 +3592,7 @@ check_clause(Env, ArgsTy, ResTy, C = {clause, P, Args, Guards, Block}, Caps) ->
             RefinedTys1 = refine_clause_arg_tys(ArgsTy, PatTys,
                                                 Guards, EnvNewest),
             RefinedTys2 = refine_mismatch_using_guards(RefinedTys1, C,
-                                                       EnvNewest#env.venv, EnvNewest),
+                                                       Env#env.venv, EnvNewest),
             {RefinedTys2
             ,union_var_binds([VarBinds1, VarBinds2, EnvNewest], EnvNewest)
             ,constraints:combine(Cs1, Cs2)};

From c6f507d96e093cc545e9fef18da08c0bc29236d2 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 15 Oct 2022 00:12:49 +0200
Subject: [PATCH 19/24] Add some check_clauses_intersection trace patterns

---
 src/gradualizer_tracer.erl | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/gradualizer_tracer.erl b/src/gradualizer_tracer.erl
index c580fc0a..d546feb3 100644
--- a/src/gradualizer_tracer.erl
+++ b/src/gradualizer_tracer.erl
@@ -145,6 +145,17 @@ start() ->
     %dbg:tpl(typechecker, normalize, x),
     %dbg:tpl(typechecker, do_add_types_pats, x),
 
+    %dbg:tpl(typechecker, check_clauses_intersection, []),
+    %dbg:tpl(typechecker, check_reachable_clauses, x),
+    %dbg:tpl(typechecker, check_clause, x),
+    %dbg:tpl(typechecker, check_arg_exhaustiveness, x),
+    %dbg:tpl(typechecker, check_clauses_intersection_throw_if_seen, x),
+    %dbg:tpl(typechecker, refine_clause_arg_tys, x),
+    %dbg:tpl(typechecker, refine_mismatch_using_guards, x),
+    %dbg:tpl(typechecker, are_patterns_matching_all_input, x),
+    %dbg:tpl(typechecker, check_guard_call, x),
+    %dbg:tpl(typechecker, type_diff, x),
+
     %dbg:tpl(?MODULE, debug, x),
     %dbg:tpl(erlang, throw, x),
 

From 3f398fdd9a9b3859d25b88119e1b16d9f15d26ee Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Sat, 15 Oct 2022 00:20:51 +0200
Subject: [PATCH 20/24] Add refine_ty(list(_), list(any())) clause

---
 src/typechecker.erl | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index f2ef8eb1..a7677460 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -3792,6 +3792,8 @@ refine_ty(?type(nil), ?type(list, _), _, _Env) ->
 refine_ty(?type(nonempty_list, _), ?type(list, [?type(any)]), _, _Env) ->
     %% The guard is_list/1 catches every nonempty list
     type(none);
+refine_ty(?type(list, _), ?type(list, [?type(any)]), _, _Env) ->
+    type(none);
 refine_ty(?type(nonempty_list, [Ty1]), ?type(nonempty_list, [Ty2]), Trace, Env) ->
     case refine(Ty1, Ty2, Trace, Env) of
         ?type(none) ->

From e584d57427ae26c333b1f7565d15d20450f7d7a8 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Thu, 20 Oct 2022 18:43:23 +0200
Subject: [PATCH 21/24] Refactor and document check_clauses_intersection/5

---
 src/typechecker.erl | 118 ++++++++++++++++++++++++++++++--------------
 1 file changed, 80 insertions(+), 38 deletions(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index a7677460..6aee0d6e 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -3395,7 +3395,7 @@ check_clauses_intersect(Env, Tys, Clauses) ->
     RefinedArgsTyss = maps:from_list(lists:map(fun ({ArgsTys, _}) ->
                                                        {ArgsTys, ArgsTys}
                                                end, FunTys)),
-    check_clauses(Env, {intersection, FunTys}, {Clauses, #{}, RefinedArgsTyss}, Clauses, bind_vars).
+    check_clauses_intersection(Env, FunTys, {Clauses, #{}, RefinedArgsTyss}, Clauses, bind_vars).
 
 check_clauses_union(_Env, [], _Clauses) ->
     %% TODO: Improve quality of type error
@@ -3408,61 +3408,105 @@ check_clauses_union(Env, [Ty|Tys], Clauses) ->
             check_clauses_union(Env, Tys, Clauses)
     end.
 
-%% Checks a list of clauses (if/case/fun/try/catch/receive).
--spec check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) -> R when
+%% Checks a list of function clauses against an intersection type (multiple-clause spec).
+-spec check_clauses_intersection(Env, SpecClauses, Acc, Clauses, Caps) -> R when
       Env :: env(),
-      ArgsTy :: [type()] | {intersection, [{[type()], type()}]},
-      ResTy :: type() | {{intersection, [{[type()], type()}]}, #{}},
-      Clauses :: [gradualizer_type:abstract_clause(), ...],
+      SpecClauses :: [{[type()], type()}],
+      Acc :: {OrigClauses, Seen, RefinedArgsTyss},
+      OrigClauses :: [gradualizer_type:abstract_clause(), ...],
+      Seen :: map(),
+      RefinedArgsTyss :: #{[type()] := [type()]},
+      Clauses :: [gradualizer_type:abstract_clause()],
       Caps :: capture_vars | bind_vars,
       R :: {env(), constraints:constraints()}.
-check_clauses(Env, {intersection, []}, _Acc, _Clauses, _Caps) ->
-    %% TODO: return the right constraints
+check_clauses_intersection(Env, [] = _SpecClauses, _Acc, _Clauses, _Caps) ->
+    %% `SpecClauses' are empty - the function is checked without errors.
+    %% TODO: return the right constraints - we should store them in Acc
     {Env, constraints:empty()};
-check_clauses(Env, {intersection, [{ArgsTys, _ResTy} = FunTy | FunTys]},
-              {OrigClauses, Seen, RefinedArgsTyss},
-              [] = _Clauses, _Caps) ->
-    check_clauses(Env, {intersection, [FunTy | FunTys]},
-                  {OrigClauses, maps:put(ArgsTys, hd(OrigClauses), Seen), RefinedArgsTyss},
-                  OrigClauses, _Caps);
-check_clauses(Env, {intersection, [{ArgsTys, ResTy} = FunTy | FunTys]},
-              {OrigClauses, Seen, RefinedArgsTyss},
-              [Clause | Clauses], Caps) ->
+check_clauses_intersection(Env, [{ArgsTys, _ResTy} = SpecClause | SpecClauses],
+                           {OrigClauses, Seen, RefinedArgsTyss},
+                           [] = _Clauses, _Caps) ->
+    %% `SpecClauses' are not empty, but `Clauses' are empty.
+    %% Let's consider the following code:
+    %%
+    %% -spec h(t()) -> string();
+    %%        ([t()]) -> [string()].
+    %% h(Types) when is_list(Types) -> lists:map(fun h/1, Types);
+    %% h({tag, _}) -> "".
+    %%
+    %% We'll reach this `check_clauses_intersection' clause when we've already
+    %% checked `(t()) -> string()' and we're looking at `([t()]) -> string()'.
+    %% In order to check `(t()) -> string()' we had to go through all `h/1' clauses,
+    %% so `Clauses' is empty.
+    %% To find clauses matching `([t()]) -> string()' we have to start over with `OrigClauses'.
+    check_clauses_intersection(Env, [SpecClause | SpecClauses],
+                               {OrigClauses, maps:put(ArgsTys, hd(OrigClauses), Seen), RefinedArgsTyss},
+                               OrigClauses, _Caps);
+check_clauses_intersection(Env, [{ArgsTys, ResTy} = SpecClause | SpecClauses],
+                           {OrigClauses, Seen, RefinedArgsTyss},
+                           [Clause | Clauses], Caps) ->
+    %% `SpecClauses' is not empty and `Clauses' is not empty either.
+    %% Now considering:
+    %%
+    %% -spec g2(t()) -> string();
+    %%         ([t()]) -> [string()].
+    %% g2([] = _Types) -> [];
+    %% g2({tag, _}) -> "";
+    %% g2([_|_] = Types) -> lists:map(fun g2/1, Types).
+    %%
+    %% We're in the general case, for example checking
+    %% `g2([_|_] = _Types) -> []' against `([t()]) -> [string()]'.
+    %%
+    %% First, we have to check if there's already any refinement recorded for `ArgsTys :: [t()]'.
     MaybeRefinedArgsTys = maps:get(ArgsTys, RefinedArgsTyss),
-    case check_clauses_throw_if_already_seen(ArgsTys, MaybeRefinedArgsTys, Clause, Seen, Env) of
-        done ->
-            {Env, constraints:empty()};
+    %% We also have to check if we've already seen this `{ArgsTys, Clause}' pair.
+    %% If that's the case, we have to fail to prevent cycling indefinitely.
+    case check_clauses_intersection_throw_if_seen(ArgsTys, MaybeRefinedArgsTys, Clause, Seen, Env) of
         {type_error, E} ->
             throw(E);
         ok ->
-
             Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
-            %% Clauses for if, case, functions, receive, etc.
-
             try check_clause(Env1, MaybeRefinedArgsTys, ResTy, Clause, Caps) of
-                {[?type(none) | _] = RefinedArgsTys, Env2, Cs} ->
+                {[?type(none) | _] = RefinedArgsTys, _Env2, _Cs} ->
+                    %% We've exhausted this `SpecClause'. Check remaining `SpecClauses'.
+                    %% TODO: don't drop the constraints
                     RefinedArgsTyss1 = maps:put(ArgsTys, RefinedArgsTys, RefinedArgsTyss),
                     Seen1 = maps:put({ArgsTys, Clause}, true, Seen),
-                    check_clauses(Env1, {intersection, FunTys},
-                                  {OrigClauses, Seen1, RefinedArgsTyss1},
-                                  OrigClauses, Caps);
-                {RefinedArgsTys, Env2, Cs} ->
+                    check_clauses_intersection(pop_clauses_controls(Env1),
+                                               SpecClauses,
+                                               {OrigClauses, Seen1, RefinedArgsTyss1},
+                                               OrigClauses, Caps);
+                {RefinedArgsTys, _Env2, _Cs} ->
+                    %% We've not exhausted this `SpecClause', so continue with the next `Clauses'.
+                    %% TODO: don't drop the constraints
                     RefinedArgsTyss1 = maps:put(ArgsTys, RefinedArgsTys, RefinedArgsTyss),
                     Seen1 = maps:put({ArgsTys, Clause}, true, Seen),
-                    check_clauses(Env1, {intersection, [FunTy | FunTys]},
-                                  {OrigClauses, Seen1, RefinedArgsTyss1},
-                                  Clauses, Caps)
+                    check_clauses_intersection(pop_clauses_controls(Env1),
+                                               [SpecClause | SpecClauses],
+                                               {OrigClauses, Seen1, RefinedArgsTyss1},
+                                               Clauses, Caps)
             catch
                 E when element(1, E) =:= type_error ->
                     %% We've not exhausted this spec clause, but we've got a type error,
                     %% e.g. a pattern in the function head doesn't match the spec.
+                    %% We'll rethrow this error if we ever cycle back to this
+                    %% `SpecClause' / `Clause' combination.
                     Seen1 = maps:put({ArgsTys, Clause}, E, Seen),
-                    check_clauses(Env1, {intersection, [FunTy | FunTys]},
-                                  {OrigClauses, Seen1, RefinedArgsTyss},
-                                  Clauses, Caps)
+                    check_clauses_intersection(pop_clauses_controls(Env1),
+                                               [SpecClause | SpecClauses],
+                                               {OrigClauses, Seen1, RefinedArgsTyss},
+                                               Clauses, Caps)
             end
+    end.
 
-    end;
+%% Checks a list of clauses (if/case/fun/try/catch/receive) against a single-clause spec.
+-spec check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) -> R when
+      Env :: env(),
+      ArgsTy :: [type()] | {intersection, [{[type()], type()}]},
+      ResTy :: type() | {{intersection, [{[type()], type()}]}, #{}},
+      Clauses :: [gradualizer_type:abstract_clause(), ...],
+      Caps :: capture_vars | bind_vars,
+      R :: {env(), constraints:constraints()}.
 check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
     %% This is fine, since we handle the other option in the clause above.
@@ -3474,12 +3518,10 @@ check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env3 = pop_clauses_controls(Env2),
     {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}.
 
-check_clauses_throw_if_already_seen(ArgsTys, RefinedArgsTy, Clause, Seen, Env) ->
+check_clauses_intersection_throw_if_seen(ArgsTys, RefinedArgsTy, Clause, Seen, Env) ->
     case maps:get({ArgsTys, Clause}, Seen, false) of
         false ->
             ok;
-        ok ->
-            done;
         true ->
             {clause, P, _, _, _} = Clause,
             throw(nonexhaustive(P, gradualizer_lib:pick_values(RefinedArgsTy, Env)));

From 4ef3c85481a20991d0cce85854c343e1a7ead3ff Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Thu, 20 Oct 2022 19:14:58 +0200
Subject: [PATCH 22/24] Simplify check_reachable_clauses()

---
 src/typechecker.erl | 33 +++++++++------------------------
 1 file changed, 9 insertions(+), 24 deletions(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index 6aee0d6e..46e1127c 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -3513,7 +3513,7 @@ check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     ArgsTy = ?assert_type(ArgsTy, [type()]),
     %% Clauses for if, case, functions, receive, etc.
     {VarBindsList, Css, RefinedArgsTy, Env2} =
-        check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTy, Env1, throw),
+        check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTy, Env1),
     check_arg_exhaustiveness(Env2, ArgsTy, Clauses, RefinedArgsTy),
     Env3 = pop_clauses_controls(Env2),
     {union_var_binds(VarBindsList, Env3), constraints:combine(Css)}.
@@ -3529,30 +3529,15 @@ check_clauses_intersection_throw_if_seen(ArgsTys, RefinedArgsTy, Clause, Seen, E
             {type_error, ClauseError}
     end.
 
-%% We return `{remaining_clauses, _, _, _, _}' either because of exhaustion of the current spec clause
-%% or because we failed matching a function clause pattern to the spec clause.
-check_reachable_clauses(_ResTy, [], _Caps, VBs, Cs, RefinedArgsTys, Env, _) ->
+check_reachable_clauses(_ResTy, [], _Caps, VBs, Cs, RefinedArgsTys, Env) ->
     {VBs, Cs, RefinedArgsTys, Env};
-check_reachable_clauses(_ResTy, Clauses, _Caps, _, _, [?type(none)|_] = RefinedArgsTys, Env, Action) ->
-    %% We've exhausted this spec clause by matching the function clauses,
-    %% but there are still more function clauses to check.
-    case Action of
-        throw -> throw(type_error(unreachable_clauses, Clauses));
-        return -> {remaining_clauses, Clauses, RefinedArgsTys, Env, ok}
-    end;
-check_reachable_clauses(ResTy, [Clause | Clauses], Caps, VBs, Css, RefinedArgsTys, EnvIn, Action) ->
-    try check_clause(EnvIn, RefinedArgsTys, ResTy, Clause, Caps) of
-        {NewRefinedArgsTys, Env2, Cs} ->
-            VB = refine_vars_by_mismatching_clause(Clause, EnvIn#env.venv, Env2),
-            check_reachable_clauses(ResTy, Clauses, Caps, [Env2 | VBs], [Cs | Css],
-                                    NewRefinedArgsTys, Env2#env{venv = VB}, Action)
-    catch
-        E when element(1, E) =:= type_error andalso Action =:= return ->
-            %% We've not exhausted this spec clause, but we've got a type error,
-            %% e.g. a pattern in the function head doesn't match the spec.
-            %% We return to try with the remaining spec clauses.
-            {remaining_clauses, [Clause | Clauses], RefinedArgsTys, EnvIn, E}
-    end.
+check_reachable_clauses(_ResTy, Clauses, _Caps, _, _, [?type(none)|_], _Env) ->
+    throw(type_error(unreachable_clauses, Clauses));
+check_reachable_clauses(ResTy, [Clause | Clauses], Caps, VBs, Css, RefinedArgsTys, EnvIn) ->
+    {NewRefinedArgsTys, Env2, Cs} = check_clause(EnvIn, RefinedArgsTys, ResTy, Clause, Caps),
+    VB = refine_vars_by_mismatching_clause(Clause, EnvIn#env.venv, Env2),
+    check_reachable_clauses(ResTy, Clauses, Caps, [Env2 | VBs], [Cs | Css],
+                            NewRefinedArgsTys, Env2#env{venv = VB}).
 
 push_clauses_controls(#env{} = Env, #clauses_controls{} = CC) ->
     ?verbose(Env, "Pushing ~p~n", [CC]),

From f326c403314a25ed90adc807136e850d55b5f974 Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Thu, 20 Oct 2022 19:38:52 +0200
Subject: [PATCH 23/24] Drop the overspec

---
 src/typechecker.erl | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/typechecker.erl b/src/typechecker.erl
index 46e1127c..e5b726c1 100644
--- a/src/typechecker.erl
+++ b/src/typechecker.erl
@@ -3502,15 +3502,13 @@ check_clauses_intersection(Env, [{ArgsTys, ResTy} = SpecClause | SpecClauses],
 %% Checks a list of clauses (if/case/fun/try/catch/receive) against a single-clause spec.
 -spec check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) -> R when
       Env :: env(),
-      ArgsTy :: [type()] | {intersection, [{[type()], type()}]},
-      ResTy :: type() | {{intersection, [{[type()], type()}]}, #{}},
+      ArgsTy :: [type()],
+      ResTy :: type(),
       Clauses :: [gradualizer_type:abstract_clause(), ...],
       Caps :: capture_vars | bind_vars,
       R :: {env(), constraints:constraints()}.
 check_clauses(Env, ArgsTy, ResTy, Clauses, Caps) ->
     Env1 = push_clauses_controls(Env, #clauses_controls{exhaust = Env#env.exhaust}),
-    %% This is fine, since we handle the other option in the clause above.
-    ArgsTy = ?assert_type(ArgsTy, [type()]),
     %% Clauses for if, case, functions, receive, etc.
     {VarBindsList, Css, RefinedArgsTy, Env2} =
         check_reachable_clauses(ResTy, Clauses, Caps, [], [], ArgsTy, Env1),

From 6a9e54e2611afe9ec7d70d97ffc45bc1d65a834a Mon Sep 17 00:00:00 2001
From: Radek Szymczyszyn <radoslaw.szymczyszyn@erlang-solutions.com>
Date: Thu, 20 Oct 2022 20:29:38 +0200
Subject: [PATCH 24/24] Fix specs in tests

---
 .../should_fail/spec_and_fun_clause_intersection_fail.erl | 2 +-
 .../should_pass/spec_and_fun_clause_intersection_pass.erl | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/test/should_fail/spec_and_fun_clause_intersection_fail.erl b/test/should_fail/spec_and_fun_clause_intersection_fail.erl
index bda38573..09e733dd 100644
--- a/test/should_fail/spec_and_fun_clause_intersection_fail.erl
+++ b/test/should_fail/spec_and_fun_clause_intersection_fail.erl
@@ -14,7 +14,7 @@ f({tag, _}) -> "".
 g([] = _Types) -> "";
 g({tag, _}) -> "".
 
--spec i([t()]) -> string();
+-spec i([t()]) -> [string()];
        (t()) -> string().
 i([_|_] = Types) -> lists:map(fun i/1, Types);
 i({tag, _}) -> "".
diff --git a/test/should_pass/spec_and_fun_clause_intersection_pass.erl b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
index c1c350f0..8d000246 100644
--- a/test/should_pass/spec_and_fun_clause_intersection_pass.erl
+++ b/test/should_pass/spec_and_fun_clause_intersection_pass.erl
@@ -11,7 +11,7 @@ f([_|_]) -> qux.
 -type t() :: {tag, integer()}.
 
 %% Order of spec clauses matches the order of patterns in function clauses - this should pass.
--spec g([t()]) -> string();
+-spec g([t()]) -> [string()];
        (t()) -> string().
 g([] = _Types) -> [];
 g([_|_] = Types) -> lists:map(fun g/1, Types);
@@ -20,7 +20,7 @@ g({tag, _}) -> "".
 %% Order of spec clauses doesn't match the order of patterns
 %% in function clauses - this should pass, too.
 -spec g1(t()) -> string();
-        ([t()]) -> string().
+        ([t()]) -> [string()].
 g1([] = _Types) -> [];
 g1([_|_] = Types) -> lists:map(fun g1/1, Types);
 g1({tag, _}) -> "".
@@ -28,12 +28,12 @@ g1({tag, _}) -> "".
 %% Order of spec clauses doesn't match the order of patterns
 %% in function clauses and function clause patterns are mixed - will that pass?
 -spec g2(t()) -> string();
-        ([t()]) -> string().
+        ([t()]) -> [string()].
 g2([] = _Types) -> [];
 g2({tag, _}) -> "";
 g2([_|_] = Types) -> lists:map(fun g2/1, Types).
 
 -spec h(t()) -> string();
-       ([t()]) -> string().
+       ([t()]) -> [string()].
 h(Types) when is_list(Types) -> lists:map(fun h/1, Types);
 h({tag, _}) -> "".