The pattern ... does not have type: [] when matching on lists

[erszcz]

A warning of this kind pops up multiple times in the self gradualization log and seems to be connected to list/non-empty-list exhaustiveness checking. When the order of clauses is changed as below:

diff --git a/src/gradualizer.erl b/src/gradualizer.erl
index 8e89af7..f48b108 100644
--- a/src/gradualizer.erl
+++ b/src/gradualizer.erl
@@ -193,9 +193,9 @@ add_source_file_and_forms_to_opts(File, Forms, Opts) ->

 %% Extract -gradualizer(Options) from AST
 -spec options_from_forms(gradualizer_file_utils:abstract_forms()) -> options().
+options_from_forms([]) -> [];
 options_from_forms([{attribute, _L, gradualizer, Opts} | Fs]) when is_list(Opts) ->
     Opts ++ options_from_forms(Fs);
 options_from_forms([{attribute, _L, gradualizer, Opt} | Fs]) ->
     [Opt | options_from_forms(Fs)];
-options_from_forms([_F | Fs]) -> options_from_forms(Fs);
-options_from_forms([]) -> [].
+options_from_forms([_F | Fs]) -> options_from_forms(Fs).

The warning becomes:

ebin/gradualizer.beam: The clause on line 201 at column 1 cannot be reached

It refers to options_from_forms([_F | Fs]), but it's a false positive - the clause is still necessary, as removing it causes tests to fail.

This was spotted when working on #341.

[berbiche]

Hi,

I'm hitting this issue in multiple functions in a large codebase. Most functions pattern match against a list of tuples:

-spec should_not_error([{integer(), integer()}]) -> integer().
should_not_error([{A, 0} | _]) ->
    A;
%% The pattern [{A, _} | _] does not have type: []
should_not_error([{A, _} | _]) ->
    A;
should_not_error([]) ->
    0.

Applying the commit 343d4f6018f23de7a9c45b309e12aa75919be5d1 partially resolves this issue but makes a valid test fail:

%% test/should_pass/user_type_in_pattern_body.erl
-module(user_type_in_pattern_body).

%% Check that the pattern type is normalized when recursively checking a pattern

-compile([export_all, nowarn_export_all]).

-type t()  :: {}.

%% Cons: The element type t() should be normalized to {}, to check that the head
%% pattern {} has type t().
-spec cons([t()]) -> boolean().
cons([{} | _]) -> true;
cons([])        -> false.

test/should_pass/user_type_in_pattern_body.erl: Nonexhaustive patterns on line 12 at column 1
Example values which are not covered:
	[{}]

Is there a simple solution that can resolve the cons list issue?

[erszcz]

Hi, @berbiche!

I think the cons error you describe is solved by the next commit from #359, that is https://github.com/josefs/Gradualizer/pull/359/commits/bebce51d3c4aab812686e0f78f81d7f13bca4030. At commit f044c35f2701a76a6eb26d8154c0c6e76980eb49 in #359 no tests fail.

Now, there are two things to consider. The above passed all tests, but it didn't pass make gradualize - it looped indefinitely. Now that we have #383 in master, it shouldn't be the case anymore, but this is something to experiment with.

There's also another direction of work started in #376, which would simplify the code a little bit, but there's no 100% guarantee that it would resolve the problem of infinite looping on some code paths.

I think we should pursue both of the above, i.e. take the fixes from #383 and rebase them onto master, but as well refactor the code to use head normal form which Viktor started doing in #376.