Remaining self-gradualization errors

[erszcz]

This is a list of all self-gradualization errors remaining after #427.

ebin/gradualizer.beam: The operator '++' on line 154 at column 58 is expected to have type _TyVar-576460752303423291 which is too precise to be statically checked
ebin/typechecker.beam: The operator '-' on line 1711 at column 66 is expected to have type pos_integer() which is too precise to be statically checked

Not sure if this can be solved.

ebin/gradualizer_db.beam: The clause on line 356 at column 1 cannot be reached

Caused by too limited record pattern interpretation, which doesn't consider matches on exact field values. This leads to consecutive clauses being treated as matching on the same args, which is not the case.

ebin/gradualizer_lib.beam: The variable on line 170 at column 60 is expected to have type [any()] but it has type none()
ebin/typechecker.beam: The variable on line 737 at column 24 is expected to have type [any()] but it has type none()
ebin/typelib.beam: The variable on line 159 at column 71 is expected to have type [any()] but it has type none()
ebin/typelib.beam: The variable on line 189 at column 57 is expected to have type [any()] but it has type none()

A series of list comprehension related errors, stemming from the fact that vars in generators are assumed to be of type none(). Tracked as #433.

ebin/gradualizer_prelude.beam: The tuple on line 0 is expected to have type erl_parse:abstract_form() | erl_parse:form_info() but it has type {attribute, 1, file, {[$...$v, ...], 1}}

This error is caused by the fact that Gradualizer cannot infer that a literal 1 is actually an instance of erl_anno:anno(). This is the case of all the forms generated by the parse transform and injected into the compiled prelude.

ebin/typechecker.beam: The pattern any on line 586 at column 10 doesn't have the type none()

No idea what's causing this one, possibly some refinement by clause which has gone wrong.

ebin/typechecker.beam: The tuple on line 801 at column 44 is expected to have type type() but it has type {user_type, 0, atom(), [B]}

Not sure what's wrong here. If we add a type assertion like NormalizedArgs :: [type()] we get the same error, but with a list of type vars instead of [B].

ebin/typechecker.beam: The pattern {type, _, T, Args} on line 3653 at column 28 doesn't have the type type()

I have a hunch that this is caused by the annotated_type variant of type(), but haven't checked that.

ebin/typechecker.beam: The tuple on line 4789 at column 5 is expected to have type type() but it has type {type, anno(), map | tuple, any}

Error in checking function intersection types? Or a bug in the spec? Not sure. Edit: a bug in the spec, already fixed in #427.

ebin/typelib.beam: The variable on line 106 at column 71 is expected to have type [A] but it has type {ann_type, anno(), [af_anno() | abstract_type()]} |

I'm not sure what's wrong, but neither ?assert_type nor ?annotate_type helped as was the case in similar situations elsewhere. However, they do produce different error messages (type order is different).

[zuiderkwast]

Great investigation!

I think "which is too precise to be statically checked" is a really strange error. In other cases, we accept type variables as any() and add some constraint somewhere. Perhaps we should do that here too and get rid of this kind of error?

[erszcz]

I was thinking something similar. In general, the type var related bugs will only be fixable once we have a constraint solver, but we could store the constraints already instead of reporting a bug.

With the solver in place, we'll hopefully also be able to do better with function polymorphism - I'm keen on testing some examples from Bidirectional typing for Erlang with the solver, but let's first finish with these remaining self-gradualization bugs before introducing new features/bugs ;)

[zuiderkwast]

Great, yes I agree about storing the constraints now and solving them later.

(I don't know if they can be solved in a sound manner though, but that's a different topic.)

[erszcz]

For the record, this is finally solved with changes that enabled #521. Since that PR, Gradualizer can self-check with no errors reported. It's checked in CI / GH Actions for each PR or commit to master.