Experimental constraint solver

[erszcz]

This rebases #284 by @josefs onto the current master branch. It also adds some polymorphic function tests borrowed from Bidirectional typing for Erlang to show the solver works - at least in some cases.

Constraint solving is enabled by using a Gradualizer option solve_constraints. Without the option the behaviour is unchanged. I think this approach will allow to merge this PR early, yet make the functionality opt-in while it's being polished.

I'm making this PR a draft for now, since it shows some suspicious reports when running a self-check:

ebin/gradualizer_db.beam: The type 0..1114111 is not a subtype of {_TyVar-576460752303417119, _TyVar-576460752303417087}
ebin/gradualizer_db.beam: The type [char()] is not a subtype of {_TyVar-576460752303415487, _TyVar-576460752303415455}

In general, the number of warnings on a self-check has grown significantly with this change. However, that was to be expected.

[erszcz]

Actually, I don't think map_type_var should pass - as the list element type is union of a map and an atom, I think the map pattern match might fail. I'll move it around as appropriate tomorrow.

[erszcz]

I've rebased this on top of the current master and force pushed.

Solving constraints is currently enabled by a command-line flag or an option set via an attribute. It's enabled for the self-check, which bumps the number of errors above 100 lines - that's why CI fails. It's not a lot more - 116 lines - but still more than the self-imposed threshold of 100.

I'm also gathering examples that would be useful as tests (currently the poly1.erl file apart from the tests already committed under test), which allows me to understand the places where the type checker approach fails (apart from a lot of places currently just dropping constraints). One such example is:

%% false negative, i.e. there's an undetected bug here
-spec i([binary() | integer()]) -> [integer()].
i(L) ->
    map(fun
            (I) when is_integer(I) -> I * 2;
            (B) when is_list(B) -> list_to_integer(B)
        end, L).

B should be constrained to a binary, but this inconsistency is not caught. It's clear issues arise when union types, type refinement, and constraint solving overlap.

[erszcz]

I think this is ready for review now. My rationale for merging this in is that on a feature branch it's subject to bit rot, whereas on master it will be regularly tested for compatibility with the rest of the project thanks to CI.

Main changes from #284:

• a number of tests, all test files enabling constraint solving start with poly_ prefix for clarity
• locating a constraint error is more convenient:
  • constraint error messages contain type variable names
  • type variable names are deterministic and descriptive - they start with the original type var name, e.g. A_... for a (A) -> boolean() function
  • constraint error messages report the location of the top-level function for which a constraint error was identified as that's the most precise location that's available to the type checker
  • see https://github.com/josefs/Gradualizer/actions/runs/3608900282/jobs/6081768978 ("Run self check") for an example output
• number of self-check error lines < 100, i.e. we're below the self-imposed CI limit
• constraint solving is opt-in, it requires a command-line --solve_constraints flag or an in-file Gradualizer solve_constraints attribute to be enabled

Constraint solving will certainly require more work to be fully functional, especially in the light of #488, but I think it's better to have whatever already works merged to master.

@josefs @zuiderkwast WDYT?

[erszcz]

I've fixed a few more self-check errors. Do you have any comments on this, @josefs @zuiderkwast? Especially any comments vetoing a merge into master? I'd like to rebase this onto master and merge after #499.

[zuiderkwast]

The tests look good. It's nice to see that the solver does something useful.

I've only skimmed thought the implementation. I think it's a good idea to merge this with constraint solving off by default, as you suggested.

Is the solver implemented as if subtyping is transitive? This is what Josef mentioned, but I haven't really spotted this part of the implementation. It would be nice to add some example of what the solver can't do if it assumes typing is transitive, which it actually isn't when any() is involved. (X :: Y and Y :: Z doesn't imply X :: Z if Y is any()).

[zuiderkwast]

This one shouldn't fail. Should it?

[erszcz]

I don't feel completely comfortable with this topic yet, but I think it depends on the future goals: if we ever want to be able to infer the type of a function like poly_2 (for example, when it's used as an inline fun), then we're limited to rank-2 polymorphism for which inference is decidable.

According to Bidirectional Typing for Erlang:

Erlang allows higher-ranked polymorphism where polymorphic types occur anywhere in the type signature. The Hindley-Milner type inference only supports the inference of rank-1 (prenex) polymorphism. Type inference for the higher-ranked polymorphism is undecidable, which is a significant limitation for the Hindley-Milner type inference. For example, the poly_2 function shown next has rank-2 polymorphism that ETC fails to type-check:

-spec poly_2(fun((A) -> A)) -> {integer(), boolean()}.
poly_2(F) -> {F(42), F(false)}.

Similarly, ETC fails for poly_fail/3 due to its rank-2 polymorphism.

-spec poly_fail(fun((A) -> A), boolean(), integer()) -> {boolean(), integer()}.
poly_fail(F, B, I) -> {F(I), F(B)}.

In contrast, Dialyzer here finds the return type mismatch error.

As we can see from this test, Gradualizer is also able to detect this error.

I'd leave it as is until anyone of us is comfortable enough with constraint solving and polymorphism to confidently move it to should_pass tests.

[erszcz]

I've merged #499 to master and rebased this PR on top of that.

The self-check has uncovered a number of issues with functions with multiple clauses registering too narrow constraints on type variables. I came up with the idea that an argument type var should be constrained with a union of types accepted by all of such a fun's clauses. Let's consider flatmap/2 and the following example:

  -spec flatmap(Fun, List1) -> List2
                   when
                       Fun :: fun((A) -> [B]),
                       List1 :: [A],
                       List2 :: [B].

-type t1() :: {_, _, _, _}.
-type t2() :: {_, _, _}.

-spec f([t1() | t2()]) -> ok.
f(Fields) ->
    lists:flatmap(fun
                      ({_, _, _, _}) -> [t1];
                      ({_, _, _}) -> [t2]
                  end, Fields),
    ok.

When constraining A we must take all of the inline fun's clauses into account, i.e. constrain A :: {_, _, _, _} | {_, _, _}. The previous implementation used a constraint obtained from the first matching clause, which lead to Fields element t1() | t2() not type checking.

Another aspect of that can be seen in the following example:

  -spec foldl(Fun, Acc, List) -> Acc
                 when
                     Fun :: fun((T, Acc) -> Acc),
                     List :: [T].

-spec g([t1() | t2()]) -> ok.
g(Fields) ->
    lists:foldl(fun
                    ({_, _, _, _}, Acc) -> [t1 | Acc];
                    (_, Acc) -> [default | Acc]
                end, [], Fields),
    ok.

The (_, Acc) clause did not register any constraint on the first arg (_). Now, though, the catch-all clause is reflected in the union constraint as any(), i.e. the full constraint is T :: {_, _, _, _} | any().

I was afraid the idea of a union upper bound constraint might be a bit fragile, but so far it seems to work quite well 👍