WIP: Improve type checking records

[gomoripeti]

This is a work in progress. I have two questions:

I started to improve handling undefined records and record fields. But then I started to think how Gradualizer is used. In case it will be used as a parse transform (that takes place after pre-processing but before any other compiler steps) then sure these errors can happen. However if Gradualizer is used as other steps like xref, eunit, dialyzer, they are run after successful compilation. If Gradualizer works from a beam file this is surely that case. So why duplicate checks that the compiler already does. Maybe Gradualizer could just run the erlang linter (after epp) in case it works from a source file and the rest of the code can assume there are no linting errors in the AST. What do you think? (There are eg unexported functions in the should_pass examples which result in compiler warnings but Gradualizer happily checks them. I introduced undefined records but compilation fails, that's how I started to think about this)

It is possible to override/refine the types provided in the record definitions in types. eg:

-record(rec, {f1 :: atom()}).
-spec f(#rec{f1 :: foo}, term()) -> #rec{f1 :: boolean()}.
f(R, T) ->
  R#rec{f1 = is_integer(T)}.

In this case we could make use somehow of the boolean() type. Either type-check is_integer/1 both against atom() (from the record definition) and against boolean() (from the expected type) ie the intersection of atom() and boolean(). Or infer the type of the whole record update and check that against the whole ResTy.
So in general I think there are multiple flows how to verify the extra info in type-inference and type-checking flows.
Also I'm not sure if this syntax is a pure override or field type (in the above case boolean()) must strictly be a subtype of the type from the rec def (ie atom()) and whether this also needs to be checked?

[Zalastax]

It makes sense to me that we should not need to do the same checks as the compiler already does. With that said, warnings are not errors and Gradualizer should not reject typechecking a module just because there are unexported functions (it should even check unexported functions in my opinion).

[zuiderkwast]

Very nice stuff, especially the precise types.

"if we can, why not"

Well, OK, if it doesn't add complexity.

For milestone 1, I think we should really focus on code that compiles without a warning or error. With this reasoning we can postpone things like variable shadowing because it gives a compiler warning by default.

Have you considered #40 as well? I seems to be related.

[zuiderkwast]

In other words, we're checking things that we don't need, to be able to report an error that the compiler would also report.

In principle, I think it's the wrong approach, but in this case, I don't see that there might be any performance impact and the complexity of the code is the same either way, so keep it!

Reporting an exact type for record index when inference is on is very good!

[zuiderkwast]

These are not automatically tested as only one fail per module is enough for should_fail. We should really fix #129.

[zuiderkwast]

In general, please add a TODO comment when adding code to ignore unimplemented stuff.

[gomoripeti]

thank you guys for the feedback. I split this into multiple PRs

• Fix subtype checking record_field and record_index #146 to fix an error
• Fix handling undefined records and record fields #147 cosmetic change in undefined rec/field. this should be the responsibility of the compiler.
• I will work more on more precise type inference and record field type refinement

[gomoripeti]

closing this as usable parts are merged in separate PRs. There is work left in refined record types