Type refinement of map keys and values

[zuiderkwast]

Fixes #507

[erszcz]

Looks great!

[erszcz]

Ahh, I've also noticed we get a new self-check warning, but I'm not sure if it's a false-positive or actually stems from some code issue:

ebin/typechecker.beam: Lower bound [af_annotated_type() |
           af_atom() |
           af_bitstring_type() |
           af_constrained_function_type() |
           af_empty_list_type() |
           af_fun_type() |
           af_integer_range_type() |
           af_map_type() |
           af_predefined_type() |
           af_record_type() |
           af_remote_type() |
           af_singleton_integer_type() |
           af_tuple_type() |
           af_type_union() |
           af_type_variable() |
           af_user_defined_type(),
           ...] of type variable Acc_typechecker_3529_1514_typechecker_1257_1520 on line 4597 is not a subtype of any

It might be a true positive, but it's also possible that multiple constraints are registered on the type var in question leading to a conflict. I imagine it might stem from AssocTys in

        {assoc_tys, AssocTys, Cs0} ->

returned by expect_map_type being either a [type()] or any. It's handled properly by separate clauses of add_type_pat_map_key, so everything works, but the solver might not be smart enough yet to realise that. Union types - they're everywhere! Anyway, I think it's a case for another PR.

[erszcz]

I know what's going on. Since the constraints are stored in maps, and maps do not preserve the item order, the results from the constraint solver are sometimes somewhat nondeterministic (the solver iterates over one of the maps and it dictates the order in which the analysis is carried on). The error that shows up is just another manifestation of a problem that was there before this PR, too:

ebin/typechecker.beam: Lower bound default | abstract_expr() of type variable T_typechecker_3529_965_typechecker_1257_970 on line 4597 is not a subtype of non_neg_integer() | default

We can see that by comparing the results of running make gradualize vs running the typechecker directly. make gradualize:

$ export COMMIT=$(git l -1 | cut -d' ' -f1); (make gradualize | tee logs/gradualize.$COMMIT.log) && wc -l logs/gradualize.$COMMIT.log
bin/gradualizer --infer --solve_constraints --specs_override_dir priv/extra_specs/ \
        -pa ebin --color ebin | grep -v -f gradualize-ignore.lst
...
ebin/typechecker.beam: Lower bound nomatch of type variable Acc_typechecker_3529_579 on line 259 is not a subtype of {Acc_typechecker_3529_579_typechecker_1257_580,
           Acc_typechecker_3529_579_typechecker_1257_581} |
          {Acc_typechecker_3529_579_typechecker_1257_582,
           Acc_typechecker_3529_579_typechecker_1257_583}
ebin/typechecker.beam: The pattern any on line 667 at column 10 doesn't have the type none()
ebin/typechecker.beam: None of the types of the function subst_ty on line 1329 at column 55 matches the call site. Here's the types of the function:
fun((#{atom() | string() := type()}, [type()]) -> [type()])
fun((#{atom() | string() := type()}, [fun_ty()]) -> [fun_ty()])
fun((#{atom() | string() := type()}, type()) -> type())
ebin/typechecker.beam: The pattern {integer, _, Arity} on line 1849 at column 50 doesn't have the type none()
ebin/typechecker.beam: The pattern {integer, _, Arity} on line 2651 at column 50 doesn't have the type none()
ebin/typechecker.beam: The pattern {type, _, T, Args} on line 3979 at column 28 doesn't have the type type()
ebin/typechecker.beam: Lower bound [af_annotated_type() |
           af_atom() |
           af_bitstring_type() |
           af_constrained_function_type() |
           af_empty_list_type() |
           af_fun_type() |
           af_integer_range_type() |
           af_map_type() |
           af_predefined_type() |
           af_record_type() |
           af_remote_type() |
           af_singleton_integer_type() |
           af_tuple_type() |
           af_type_union() |
           af_type_variable() |
           af_user_defined_type(),
           ...] of type variable Acc_typechecker_3529_1514_typechecker_1257_1520 on line 4597 is not a subtype of any
...

bin/gradualizer:

$ ./bin/gradualizer --infer --solve_constraints --specs_override_dir priv/extra_specs/ -pa ebin -- ebin/typechecker.beam
ebin/typechecker.beam: Lower bound nomatch of type variable Acc_typechecker_3529_52 on line 259 is not a subtype of {Acc_typechecker_3529_52_typechecker_1257_53,
           Acc_typechecker_3529_52_typechecker_1257_54} |
          {Acc_typechecker_3529_52_typechecker_1257_55,
           Acc_typechecker_3529_52_typechecker_1257_56}
ebin/typechecker.beam: The pattern any on line 667 at column 10 doesn't have the type none()
ebin/typechecker.beam: None of the types of the function subst_ty on line 1329 at column 55 matches the call site. Here's the types of the function:
fun((#{atom() | string() := type()}, [type()]) -> [type()])
fun((#{atom() | string() := type()}, [fun_ty()]) -> [fun_ty()])
fun((#{atom() | string() := type()}, type()) -> type())
ebin/typechecker.beam: The pattern {integer, _, Arity} on line 1849 at column 50 doesn't have the type none()
ebin/typechecker.beam: The pattern {integer, _, Arity} on line 2651 at column 50 doesn't have the type none()
ebin/typechecker.beam: The pattern {type, _, T, Args} on line 3979 at column 28 doesn't have the type type()
ebin/typechecker.beam: Lower bound default | abstract_expr() of type variable T_typechecker_3529_965_typechecker_1257_970 on line 4597 is not a subtype of non_neg_integer() | default

We see that the last error line is reported from the same location. Since it's a known problem, I think we don't have to worry about it in this PR.

[zuiderkwast]

So we should store the constraints ordered, e.g. in a list of tuples instead of a map?

[erszcz]

Or just sort the map keys before accessing values. Yeah, I'll create a ticket not to lose track of it.