Support for rigid type variables

src/absform.erl

@@ -28,15 +28,14 @@ normalize_record_field({typed_record_field,
                         _Type} = Complete) ->
     Complete.
 
+-type bounded_fun() :: gradualizer_type:af_constrained_function_type().
+
 %% @doc Turns all function types into bounded function types. Add default empty
 %% constraints if missing.
--spec normalize_function_type_list(FunTypeList) -> FunTypeList when
-      FunTypeList :: gradualizer_type:af_function_type_list().
+-spec normalize_function_type_list(gradualizer_type:af_function_type_list()) -> [bounded_fun()].
 normalize_function_type_list(FunTypeList) ->
     ?assert_type(lists:map(fun normalize_function_type/1, FunTypeList), nonempty_list()).
 
--type bounded_fun() :: gradualizer_type:af_constrained_function_type().
-
 -spec normalize_function_type(bounded_fun()) -> bounded_fun();
                              (gradualizer_type:af_fun_type()) -> bounded_fun().
 normalize_function_type({type, _, 'bounded_fun', [_FunType, _FunConst]} = BoundedFun) ->

src/gradualizer_int.erl

@@ -54,6 +54,7 @@ is_int_subtype(Ty1, Ty2) ->
         upper_bound_more_or_eq(R2, R1).
 
 %% Greatest lower bound of two integer types.
+-spec int_type_glb(type(), type()) -> type().
 int_type_glb(Ty1, Ty2) ->
     {Lo1, Hi1} = int_type_to_range(Ty1),
     {Lo2, Hi2} = int_type_to_range(Ty2),

src/gradualizer_type.erl

@@ -30,11 +30,15 @@
               af_binary_op/1,
               af_constrained_function_type/0,
               af_constraint/0,
+              af_clause/0,
+              af_guard_seq/0,
+              af_guard/0,
               af_field_name/0,
               af_fun_type/0,
               af_function_type_list/0,
               af_record_field/1,
               af_record_field_type/0,
+              gr_any_type/0,
               af_singleton_integer_type/0,
               af_string/0,
               af_unary_op/1,
@@ -244,6 +248,7 @@
                        | af_tuple_type()
                        | af_type_union()
                        | af_type_variable()
+                       | gr_rigid_type_variable()
                        | af_user_defined_type().
 
 -type af_annotated_type() ::
@@ -308,6 +313,14 @@
 -type gr_type_var() :: atom() | string().
 -type af_type_variable() :: {'var', anno(), gr_type_var()}.
 
+%% Gradualizer: `rigid_var' is used for type variables (instead of plain `var')
+%% originating from specs of the currently checked function. They are rigid
+%% in the sense that they are fixed but completely unknown from the perspective
+%% of the function definition. We want to be able to differentiate between
+%% flexible (`var') and rigid type variables, and therefore we add this new
+%% syntactic form although they are syntactically the same.
+-type gr_rigid_type_variable() :: {'rigid_var', anno(), atom()}.
+
 -type af_user_defined_type() ::
         {'user_type', anno(), type_name(),  [abstract_type()]}.
 
@@ -338,6 +351,8 @@
                           [af_lit_atom('is_subtype') |
                            [af_type_variable() | abstract_type()]]}. % [IsSubtype, [V, T]]
 
+-type gr_any_type() :: {'type', anno(), 'any', []}.
+
 -type af_singleton_integer_type() :: af_integer()
                                    | af_character()
                                    | af_unary_op(af_singleton_integer_type())

src/typechecker.erl

@@ -527,8 +527,8 @@ compat_record_fields(_, _, _, _) ->
 
 %% Returns a successful matching of two types. Convenience function for when
 %% there were no type variables involved.
--spec ret(Seen) -> acc(Seen) when
-      Seen :: map() | type().
+-spec ret(map()) -> acc(map());
+         (type()) -> acc(type()).
 ret(Seen) ->
     {Seen, constraints:empty()}.
 
@@ -1729,14 +1729,21 @@ free_vars({type, _, _, Args}, Vars) ->
 free_vars(_, Vars) -> Vars.
 
 -spec subst_ty(#{atom() | string() := type()}, [type()]) -> [type()];
-              (#{atom() | string() := type()}, [fun_ty()]) -> [fun_ty()];
               (#{atom() | string() := type()}, type()) -> type().
 subst_ty(Sub, Tys) when is_list(Tys) ->
     [ subst_ty(Sub, Ty) || Ty <- Tys ];
 subst_ty(Sub, Ty = {var, _, X}) ->
     maps:get(X, Sub, Ty);
+subst_ty(Sub, Ty = {rigid_var, _, X}) ->
+    maps:get(X, Sub, Ty);
 subst_ty(Sub, {type, P, Name, Args}) ->
     {type, P, Name, subst_ty(Sub, Args)};
+subst_ty(Sub, {user_type, P, Name, Args}) ->
+    {user_type, P, Name, subst_ty(Sub, Args)};
+subst_ty(Sub, {remote_type, P, [Mod, Fun, Args]}) ->
+    {remote_type, P, [Mod, Fun, subst_ty(Sub, Args)]};
+subst_ty(Sub, {ann_type, P, [AnnoVar, Type]}) ->
+    {ann_type, P, [AnnoVar, subst_ty(Sub, Type)]};
 subst_ty(_, Ty) -> Ty.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -3745,6 +3752,8 @@ instantiate({var, _, TyVar}, Map) ->
         Ty ->
             {Ty, maps:new(), Map}
     end;
+instantiate(T = {rigid_var, _, _}, Map) ->
+    {T, maps:new(), Map};
 instantiate(T = ?type(_), Map) ->
     {T, maps:new(), Map};
 instantiate({type, P, Ty, Args}, Map) ->
@@ -3791,6 +3800,37 @@ instantiate_inner([Ty | Tys], Map) ->
     {[NewTy|NewTys], maps:merge(Vars, MoreVars), EvenNewerMap}.
 
 
+%% Turns all type variables in a given type into rigid type variables.
+%%
+%% We want to use rigid type variables when typechecking a polymorphic
+%% function because type variables used in its spec can be instantiated
+%% to anything by the caller, so the polymorphic function cannot make
+%% any assumptions about their type or value.
+%%
+%% 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()].
+make_rigid_type_vars(Tys) when is_list(Tys) ->
+    [ make_rigid_type_vars(Ty) || Ty <- Tys ];
+make_rigid_type_vars({var, _, '_'} = T) ->
+    T;
+make_rigid_type_vars({var, P, Var}) when is_atom(Var) ->
+    {rigid_var, P, Var};
+make_rigid_type_vars({type, _, constraint, _Args} = T) ->
+    % do no descent into function constraints (bounds)
+    T;
+make_rigid_type_vars({type, P, Tag, Args}) ->
+    {type, P, Tag, make_rigid_type_vars(Args)};
+make_rigid_type_vars({user_type, P, Tag, Args}) ->
+    {user_type, P, Tag, make_rigid_type_vars(Args)};
+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(T) ->
+    T.
+
 %% Infers (or at least propagates types from) fun/receive/try/case/if clauses.
 -spec infer_clauses(env(), [gradualizer_type:abstract_clause()]) -> R when
       R :: {type(), VarBinds :: env(), constraints:t()}.
@@ -3979,8 +4019,9 @@ check_clauses_intersection_throw_if_seen(ArgsTys, RefinedArgsTy, Clause, Seen, E
             {type_error, ClauseError}
     end.
 
--spec check_reachable_clauses(type(), Clauses, _Caps, [env()], Css, [type()], env()) -> R when
+-spec check_reachable_clauses(type(), Clauses, Caps, [env()], Css, [type()], env()) -> R when
       Clauses :: [gradualizer_type:abstract_clause()],
+      Caps :: capture_vars | bind_vars,
       Css :: [constraints:t()],
       R :: {[env()],
             [constraints:t()],
@@ -4100,7 +4141,7 @@ check_clause(Env, ArgsTy, ResTy, C = {clause, P, Args, Guards, Block}, Caps) ->
 
 %% Refine types by matching clause. MatchedTys are the types exhausted by
 %% each pattern in the previous clause.
--spec refine_clause_arg_tys([type()], [type()], _Guards, env()) -> [type()].
+-spec refine_clause_arg_tys([type()], [type()], gradualizer_type:af_guard_seq(), env()) -> [type()].
 refine_clause_arg_tys(Tys, MatchedTys, [], Env) ->
     Ty        = type(tuple, Tys),
     MatchedTy = type(tuple, MatchedTys),
@@ -4134,7 +4175,7 @@ refine_mismatch_using_guards(PatTys,
             PatTys
     end.
 
--spec do_refine_mismatch_using_guards(_Guards, [type()], _, _, env()) -> [type()].
+-spec do_refine_mismatch_using_guards(gradualizer_type:af_guard() | [], [type()], _, _, env()) -> [type()].
 do_refine_mismatch_using_guards([], PatTys, _, _, _) -> PatTys;
 do_refine_mismatch_using_guards([{call, _, {atom, _, Fun}, Args = [{var, _, Var}]} | Tail],
                                 PatTys, Pats, VEnv, Env) ->
@@ -4609,7 +4650,7 @@ no_guards({clause, _, _, Guards, _}) ->
 
 %% Refines the types of bound variables using the assumption that a clause has
 %% mismatched.
--spec refine_vars_by_mismatching_clause(_Clause, VEnv, env()) -> VEnv.
+-spec refine_vars_by_mismatching_clause(gradualizer_type:af_clause(), venv(), env()) -> venv().
 refine_vars_by_mismatching_clause({clause, _, Pats, Guards, _Block}, VEnv, Env) ->
     PatternCantFail = are_patterns_matching_all_input(Pats, VEnv),
     case Guards of
@@ -4771,7 +4812,8 @@ 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},
-            FunTyNoPos = [ typelib:remove_pos(?assert_type(Ty, type())) || Ty <- FunTy ],
+            FunTyRigid = make_rigid_type_vars(FunTy),
+            FunTyNoPos = [ typelib:remove_pos(?assert_type(Ty, type())) || Ty <- FunTyRigid ],
             Arity = clause_arity(hd(Clauses)),
             case expect_fun_type(NewEnv, FunTyNoPos, Arity) of
                 {type_error, NotFunTy} ->

src/typechecker.hrl

@@ -3,7 +3,10 @@
 
 -record(clauses_controls, {exhaust}).
 
--record(env, {fenv              = #{}   :: map(),
+-record(env, {fenv              = #{}   :: #{{atom(), arity()} =>
+                                                  [gradualizer_type:af_constrained_function_type()]
+                                                | [gradualizer_type:gr_any_type()]
+                                            },
               imported          = #{}   :: #{{atom(), arity()} => module()},
               venv              = #{}   :: typechecker:venv(),
               tenv                      :: gradualizer_lib:tenv(),

src/typelib.erl

@@ -31,15 +31,14 @@
                                 'fun',
                                 [{type, erl_anno:anno(), product, [type()]} |
                                  type()]}.
--type printable_type() :: type() |
-                          {type, erl_anno:anno(), bounded_fun,
+-type bounded_fun() :: {type, erl_anno:anno(), bounded_fun,
                                  [function_type() | [constraint()]]}.
+-type printable_type() :: type() | bounded_fun().
 
 %% @doc
 %% Pretty-print a type represented as an Erlang abstract form.
 %% @end
--spec pp_type(printable_type()) -> string();
-             ([printable_type()]) -> string().
+-spec pp_type(printable_type() | [printable_type()]) -> io_lib:chars().
 pp_type(Types = [_|_]) ->
     %% TODO: This is a workaround for the fact that a list is sometimes used in
     %% place of a type. It typically represents a function type with multiple clauses.
@@ -53,7 +52,8 @@ pp_type({type, _, bounded_fun, [FunType, []]}) ->
 pp_type(Type = {type, _, bounded_fun, _}) ->
     %% erl_pp can't handle bounded_fun in type definitions
     %% We invent our own syntax here, e.g. "fun((A) -> ok when A :: atom())"
-    Form = {attribute, erl_anno:new(0), spec, {{foo, 0}, [Type]}},
+    TypePp = type_for_erl_pp(Type),
+    Form = {attribute, erl_anno:new(0), spec, {{foo, 0}, [TypePp]}},
     TypeDef = erl_pp:form(Form),
     {match, [S]} = re:run(TypeDef, <<"-spec foo\\s*(.*)\\.\\n*$">>,
                           [{capture, all_but_first, list}, dotall]),
@@ -66,10 +66,13 @@ pp_type({var, _, TyVar}) ->
         is_atom(TyVar) -> atom_to_list(TyVar);
         is_list(TyVar) -> TyVar
     end;
+pp_type([]) ->
+    error({badarg, []});
 pp_type(Type) ->
     %% erl_pp can handle type definitions, so wrap Type in a type definition
     %% and then take the type from that.
-    Form = {attribute, erl_anno:new(0), type, {t, Type, []}},
+    TypePp = type_for_erl_pp(Type),
+    Form = {attribute, erl_anno:new(0), type, {t, TypePp, []}},
     TypeDef = erl_pp:form(Form),
     {match, [S]} = re:run(TypeDef, <<"::\\s*(.*)\\.\\n*">>,
                           [{capture, all_but_first, list}, dotall]),
@@ -84,6 +87,21 @@ pp_type(Type) ->
     %        File      -> S ++ " in " ++ File
     %end.
 
+
+%% Transform our `type()' into the standard `erl_parse:abstract_type()' that erl_pp accepts.
+-spec type_for_erl_pp(type()) -> type();
+                     (bounded_fun()) -> bounded_fun().
+type_for_erl_pp({rigid_var, P, Var}) ->
+    {var, P, Var};
+type_for_erl_pp({type, P, Tag, Args}) when is_list(Args) ->
+    {type, P, Tag, [type_for_erl_pp(Arg) || Arg <- Args]};
+type_for_erl_pp({user_type, P, Tag, Args}) ->
+    {user_type, P, Tag, [type_for_erl_pp(Arg) || Arg <- Args]};
+type_for_erl_pp({remote_type, P, [Mod, Fun, Args]}) ->
+    {remote_type, P, [Mod, Fun, [type_for_erl_pp(Arg) || Arg <- Args]]};
+type_for_erl_pp(Type) ->
+    Type.
+
 %% Looks up and prints the type M:N(P1, ..., Pn).
 debug_type(M, N, P) ->
     case gradualizer_db:get_type(M, N, P) of
@@ -114,7 +132,7 @@ remove_pos({type, _, constraint, [{atom, _, is_subtype}, Args]}) ->
     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 ->
+  when Type == atom; Type == integer; Type == char; Type == var; Type == rigid_var ->
     {Type, erl_anno:new(0), Value};
 remove_pos({user_type, Anno, Name, Params}) when is_list(Params) ->
     {user_type, anno_keep_only_filename(Anno), Name,
@@ -246,6 +264,11 @@ substitute_type_vars({var, L, Var}, TVars) ->
         #{Var := Type} -> Type;
         _              -> {var, L, Var}
     end;
+substitute_type_vars({rigid_var, L, Var}, TVars) when is_atom(Var) ->
+    case TVars of
+        #{Var := Type} -> Type;
+        _              -> {var, L, Var}
+    end;
 substitute_type_vars(Other = {type, _, T, any}, _)
   when T == tuple; T == map ->
     Other;
@@ -317,6 +340,7 @@ reduce(Fun, _, Acc, {'type', _Anno, any} = Ty)        -> Fun(Ty, Acc);
 reduce(Fun, _, Acc, pos_inf = Ty)                     -> Fun(Ty, Acc);
 reduce(Fun, _, Acc, neg_inf = Ty)                     -> Fun(Ty, Acc);
 reduce(Fun, _, Acc, {var, _, _} = Ty)                 -> Fun(Ty, Acc);
+reduce(Fun, _, Acc, {rigid_var, _, _} = Ty)           -> Fun(Ty, Acc);
 reduce(Fun, apply, Acc, Ty) ->
     {NewTy, Acc1} = Fun(Ty, Acc),
     reduce(Fun, recurse, Acc1, NewTy);

test/should_fail/opaque_fail.erl

@@ -1,7 +1,21 @@
 -module(opaque_fail).
 
--export([use_external/2]).
+-export([use_external/2, update_without_opaque/0, add_to_opaque/0, return_opaque/0]).
 
 -spec use_external(user_types:my_opaque(), integer() | undefined) -> integer().
 use_external(I, undefined) -> I;
 use_external(_, I) -> I.
+
+-spec update_without_opaque() -> ok.
+update_without_opaque() ->
+    _Val = user_types:update_opaque(3),
+    ok.
+
+-spec add_to_opaque() -> ok.
+add_to_opaque() ->
+    Val = user_types:new_opaque(),
+    Val + 1,
+    ok.
+
+-spec return_opaque() -> user_types:my_opaque().
+return_opaque() -> 3.

test/should_fail/poly_fail.erl

@@ -3,7 +3,9 @@
 %% See "Bidirectional Typing for Erlang", N. Rajendrakumar, A. Bieniusa, 2021, Section 2. Examples.
 -export([find1/0,
          poly_2/1,
-         poly_fail/3]).
+         poly_2b/1,
+         poly_fail/3,
+         poly_fail_2/3]).
 
 %% These examples don't come from the above paper.
 -export([f/1,
@@ -25,9 +27,15 @@ find1() ->
 -spec poly_2(fun((A) -> A)) -> {integer(), boolean()}.
 poly_2(F) -> {F(42), F(false)}.
 
+-spec poly_2b(fun((A) -> A)) -> {integer(), integer()}.
+poly_2b(F) -> {F(42), F(84)}.
+
 -spec poly_fail(fun((A) -> A), boolean(), integer()) -> {boolean(), integer()}.
 poly_fail(F, B, I) -> {F(I), F(B)}.
 
+-spec poly_fail_2(fun((A) -> A), boolean(), boolean()) -> {boolean(), boolean()}.
+poly_fail_2(F, B1, B2) -> {F(B2), F(B1)}.
+
 -spec f([integer(), ...]) -> atom().
 f(L) ->
     hd(L).