josefs / Gradualizer

A Gradual type system for Erlang
MIT License
613 stars 35 forks source link

Unify type_check_expr and type_check_expr_in #574

Open erszcz opened 1 month ago

erszcz commented 1 month ago

This attempts the unification discussed in #362. The are some obvious takeaways from this exercise, some already mentioned by @xxdavid in that thread:

What do I mean by the last point? Roughly speaking, to check if syntax for Expr is handled properly by the parallel impls, we need two test cases:

-spec f1() -> some_ty().
f1() ->
    Expr.

-spec f2() -> some_ty().
f2() ->
    X = Expr,
    X.

Where in f1 type_check_expr_in would check that Expr :: some_ty() and in f2 type_check_expr would infer the type of Expr to assign it to X and only then check if X :: some_ty(). This is not obvious nor documented anywhere and I think it has lead to the disparity in syntax support in the two impls. From this perspective, merging the two seems to be compelling.

In order to make tests pass in this draft some tests had to be disabled or moved to known problems. I think that if we want to unify these parallel impls, we should bring them all into should pass/fail categories in this PR.

erszcz commented 1 month ago

Note for self - an example of a class of the self-check errors we now see is this:

$ cat tzt.erl
-module(tzt).

-type options() :: proplists:proplist().

-spec parse_opts([string()], options()) -> {[string()], options()}.
parse_opts([], Opts) ->
    {[], Opts};
parse_opts([A | Args], Opts) ->
    case A of
        "-h"                       -> {[], [help]};
        "--help"                   -> {[], [help]};
        "--verbose"                -> parse_opts(Args, [verbose | Opts])
    end.
$ ./bin/gradualizer tzt.erl
tzt.erl: The list on line 12 at column 56 is expected to have type options() but it has type [verbose | property(), ...]

        "-h"                       -> {[], [help]};
        "--help"                   -> {[], [help]};
        "--verbose"                -> parse_opts(Args, [verbose | Opts])
                                                       ^^^^^^^^^^^^^^^^

but

$ r3 shell
1> OptionTy1 = gradualizer:type("[verbose | proplists:property(), ...]").
{type,0,nonempty_list,
      [{type,0,union,
             [{atom,0,verbose},
              {remote_type,0,
                           [{atom,1,proplists},{atom,1,property},[]]}]}]}
2> OptionTy2 = gradualizer:type("gradualizer:options()").
{remote_type,0,[{atom,1,gradualizer},{atom,1,options},[]]}
3> typechecker:subtype(OptionTy1, OptionTy2, gradualizer:env()).
true
4>

Verbose log:

$ ./bin/gradualizer --verbose tzt.erl
Checking module tzt
Spawning async task...
Checking function parse_opts/2
Pushing {clauses_controls,true}
6:1: Checking clause :: {[string()], options()}
6:16: Setting var type Opts :: [property()]
7:6: Propagated type of [] :: []
7:10: Propagated type of Opts :: [property()]
7:5: Propagated type of {[], Opts} :: {[], [property()]}
7:5: Checking that {[], Opts} :: {[string()], options()}
8:1: Checking clause :: {[string()], options()}
8:13: Setting var type A :: [char()]
8:17: Setting var type Args :: [] | [string(), ...]
8:24: Setting var type Opts :: [property()]
9:10: Propagated type of A :: [char()]
10:40: Propagated type of [] :: []
10:45: Propagated type of help :: help
10:49: Propagated type of [] :: []
10:44: Propagated type of [help] :: [help, ...]
10:39: Propagated type of {[], [help]} :: {[], [help, ...]}
11:40: Propagated type of [] :: []
11:45: Propagated type of help :: help
11:49: Propagated type of [] :: []
11:44: Propagated type of [help] :: [help, ...]
11:39: Propagated type of {[], [help]} :: {[], [help, ...]}
12:50: Propagated type of Args :: [] | [string(), ...]
12:50: Checking that Args :: [string()]
12:57: Propagated type of verbose :: verbose
12:67: Propagated type of Opts :: [property()]
12:56: Propagated type of [verbose | Opts] :: [verbose | property(), ...]
12:56: Checking that [verbose | Opts] :: options()
Task returned from function parse_opts/2 with [{type_error,
                                                {cons,
                                                 {12,56},
                                                 {atom,{12,57},verbose},
                                                 {var,{12,67},'Opts'}},
                                                {type,0,nonempty_list,
                                                 [{type,0,union,
                                                   [{atom,0,verbose},
                                                    {user_type,
                                                     [{file,"proplists.erl"},
                                                      {location,0}],
                                                     property,[]}]}]},
                                                {user_type,0,options,[]}}]
tzt.erl: The list on line 12 at column 56 is expected to have type options() but it has type [verbose | property(), ...]

        "-h"                       -> {[], [help]};
        "--help"                   -> {[], [help]};
        "--verbose"                -> parse_opts(Args, [verbose | Opts])
                                                       ^^^^^^^^^^^^^^^^