Make rigid vars also from type vars in function constraints

The following type spec from gradualizer_db uses a type variables (K)
as a bound for another type variable (Key):

    -spec add_entries_to_map([{Key, Value}], #{K => V}) -> #{K => V}
                                             when Key :: K, Value :: V.

Until now, we converted all Ks and Vs to rigid vars, but then Key
and Value got replaced to plain vars K and S in solve_bounds/2.

We must therefore convert the type variables to rigid type variables
*after* the call to solve_bounds/2, which is what this commit does.

src/typechecker.erl

@@ -3985,7 +3985,8 @@ get_atom(_Env, _) ->
 %% Variables inside function constraints (e.g., `List' in the type fragment
 %% `when List :: [term()]') are kept as they are, i.e., `var'.
 -spec make_rigid_type_vars(type()) -> type();
-                          ([type()]) -> [type()].
+                          ([type()]) -> [type()];
+                          (fun_ty()) -> fun_ty().
 make_rigid_type_vars(Tys) when is_list(Tys) ->
     [ make_rigid_type_vars(Ty) || Ty <- Tys ];
 make_rigid_type_vars({var, _, '_'} = T) ->
@@ -4003,6 +4004,12 @@ make_rigid_type_vars({remote_type, P, [Mod, Fun, Args]}) ->
     {remote_type, P, [Mod, Fun, make_rigid_type_vars(Args)]};
 make_rigid_type_vars({ann_type, P, [AnnoVar, Type]}) ->
     {ann_type, P, [AnnoVar, make_rigid_type_vars(Type)]};
+make_rigid_type_vars({fun_ty, ArgTys, ResTy, Cs}) ->
+    {fun_ty, make_rigid_type_vars(ArgTys), make_rigid_type_vars(ResTy), Cs};
+make_rigid_type_vars({fun_ty_intersection, FunTys, Cs}) ->
+    {fun_ty_intersection, make_rigid_type_vars(FunTys), Cs};
+make_rigid_type_vars({fun_ty_union, FunTys, Cs}) ->
+    {fun_ty_union, make_rigid_type_vars(FunTys), Cs};
 make_rigid_type_vars(T) ->
     T.
 
@@ -4990,15 +4997,15 @@ type_check_function(Env, {function, _Anno, Name, NArgs, Clauses}) ->
     case maps:find({Name, NArgs}, Env#env.fenv) of
         {ok, FunTy} ->
             NewEnv = Env#env{current_spec = FunTy},
-            FunTyRigid = make_rigid_type_vars(FunTy),
-            FunTyNoPos = [ typelib:remove_pos(?assert_type(Ty, type())) || Ty <- FunTyRigid ],
+            FunTyNoPos = [ typelib:remove_pos(?assert_type(Ty, type())) || Ty <- FunTy ],
             Arity = clause_arity(hd(Clauses)),
             case expect_fun_type(NewEnv, FunTyNoPos, Arity) of
                 {type_error, NotFunTy} ->
                     %% This can only happen if `create_fenv/2' creates garbage.
                     erlang:error({invalid_function_type, NotFunTy});
                 FTy ->
-                    {_Vars, Cs} = check_clauses_fun(NewEnv, FTy, Clauses),
+                    FTy1 = make_rigid_type_vars(FTy),
+                    {_Vars, Cs} = check_clauses_fun(NewEnv, FTy1, Clauses),
                     {NewEnv, Cs}
             end;
         error ->

test/should_fail/rigid_type_variables_fail.erl

@@ -47,14 +47,19 @@ bad_filter([X | Xs], F) ->
 bad_map([], _F) -> [];
 bad_map([X | Xs], F) -> [F([X]) | bad_map(Xs, F)].
 
+% gets rewritten to (integer()) -> integer()
+-spec rewrite_bound(atom()) -> Int when Int :: integer().
+rewrite_bound(Atom) -> Atom.
+
+-spec bad_id_with_bound(A) -> R when R :: A.
+bad_id_with_bound(_X) -> 42.
+
 -type tagged(Value) :: {tag, Value}.
 % fails due to {inner_tag, _} not being a subtype of map()
 -spec bad_add_tag(Value) -> tagged(Value) when Value :: map().
 bad_add_tag(Value) ->
     {tag, {inner_tag, Value}}.
 
-
-
 %% All four these poly_2 examples come from the paper
 %% "Bidirectional Typing for Erlang", N. Rajendrakumar, A. Bieniusa, 2021, Section 2. Examples.
 %% These functions are not well typed according to Gradualizer, as we adopt the standard interpretation

test/should_pass/rigid_type_variables.erl

@@ -45,6 +45,9 @@ map([X | Xs], F) -> [F(X) | map(Xs, F)].
 -spec rewrite_bound(Int) -> Int when Int :: integer().
 rewrite_bound(N) -> N + 1.
 
+-spec id_with_bound(A) -> R when R :: A.
+id_with_bound(X) -> X.
+
 -type tagged(Value) :: {tag, Value}.
 % gets rewritten to (map()) -> {tag, map()}
 -spec add_tag(Value) -> tagged(Value) when Value :: map().