Refactor type_check_logic_op[_in]

[gomoripeti]

Fixes self-check warning:
The operator 'andalso' on line 1733 is given a non-boolean argument of type ok

Type checking can still return false warnings in some scenarios described in #23

[josefs]

Frankly, I'm not a fan of this change. If people want to use the second argument of lazy boolean operators for something other than a boolean, then they should use any().

Though, the xor operator should obviously be added.

[gomoripeti]

thanks @josefs for the feedback. I opened this PR (and not pushing straight) exactly to get feedback. I will rework accordingly.

So the way forward is that if people use the lazy bool ops with a non-bool in a fully untyped program, they will get a warning. Then they need to add type annotation in the right place to address the warning.
However this type annotation might need to be added to expressions, not just on function top level. Which is a longer-term feature I guess. (the ty.erl module is related)

[josefs]

@gomoripeti , I'm not quite sure what you mean by "if people use the lazy bool ops with a non-bool in a fully untyped program, they will get a warning". Right now, if a programmer doesn't specify any types, then there will be no errors or warnings when e.g. passing a non-boolean second argument to andalso. It works just fine!

It is when adding type annotations that the programmer has to be careful, if s/he wants to keep using a non-boolean argument then there needs to be an any() type at some appropriate place to make sure the gradualizer doesn't complain. But I think you understand this part already.

[gomoripeti]

Actually in some cases there is a type error even without type annotation, eg:

f() -> false andalso {true}.

=> The operator 'andalso' on line 1 is given a non-boolean argument of type {any()}

It depends on whether type_check_expr infers some type for the expression or just returns any() (in most of the cases the later)

A more practical example is when the second argument is a library function which happens to be typed within OTP, (this case is not exactly non-typed, but the type annotation of the called function is out of the control of the developer) eg:

f() -> true andalso atom_to_list(asd).

=> The operator 'andalso' on line 1 is given a non-boolean argument of type string()

Can these examples be considered bugs, so the correct behaviour should be as you described?

[josefs]

The first example is clearly a bug and I'm surprised that the gradualizer complains here. Good find!

As for the second example, it's behaving as intended. The function f/0 may not have a type spec, but atom_to_list/1 does, so that type information should be propagated. I was not very careful when writing "if a programmer doesn't specify any types". I meant something more along these lines: if there are no type specs in the program, or in any of the library functions that are called, then there will be no errors or warnings.

[zuiderkwast]

It is not true then that any untyped program can start using gradualizer without getting any type errors, and then gradually add specs. Most OTP library functions are speced already.

It seems a bit weird that the above examples give type errors but this one doesn't:

f() -> foo andalso banana.

I think that not propagating any types, not even the return types from spec'ed functions, would be more intuitive for type_check_expr if we want to stick to "if a programmer doesn't specify any types". If we do propagate types, then why not also propagate the type of literals? Library functions are outside the programmer's control, just like literals and other language constructs.

[josefs]

@zuiderkwast you make a good point about OTP being annotated. I think we should consider having a flag to gradualizer which can effectively turn off type annotations in OTP. That will allow programmers to start from a clean slate with absolutely no type annotations in their (possibly already existing) projects and then gradually add type information.

[zuiderkwast]

Such a flag @josef, would it turn off type annotation only in OTP or also in 3rd party libraries? I think that most projects use 3rd party libraries and that these most often are annotated too.

Would the type annotations be turned off only in type_check_expr but still use them in type_check_expr_in? I think that would probably be good, but I wouldn't mind some more reasoning about it.

Thanks @gomoripeti for creating separate issues for each topic! Let's continue discussion in e.g. #26?

[josefs]

@zuiderkwast, yes, I think it'd make sense to silence the type specs in 3rd party libraries as well. But that could possibly be another flag.

As for where the type specs would be silenced, I'd imagine it would be everywhere. I think it would be rather hard to explain the effects of having the type spec only be turned off in type_check_expr.

[gomoripeti]

As concluded in #23 and also on erlang mailing list short-circuit operators should not support any term() type as second argument. It is only an implementation detail that there is no check in the VM for the type of the second arg (which is an optimisation to allow tail recursion) and it is considered a bad practice to exploit this.

Therefore closing this PR and will submit a new one which fixes warnings like:
The operator 'andalso' on line ... is given a non-boolean argument of type true | false