Type refinement of list tails

[gomoripeti]

Currently type checking the following snippet (simplified version of lists:droplast/1)

-spec droplast(nonempty_list(T)) -> list(T).
droplast([_T])  -> [];
droplast([H|T]) -> [H|droplast(T)].

fails with

The variable 'T' has type [] | [any(), ...] but is expected to have type [any(), ...]

Gradualizer does not recognize that the first clause covers the case when the tail of the cons is nil. Of course there is no type currently to describe this.

Maybe there could be an internal-only type or structure cons(HeadTy, TailTy) (already referred to in https://github.com/josefs/Gradualizer/issues/110) or sized_list(ElemTy, Size :: IntOrRange) to capture type info about list sizes.

[zuiderkwast]

If we introduce a type cons(H, T) (like a 2-tuple), we get pretty powerful things. It can be used as a primitive to define the list types:

-type list(A) :: cons(A, list(A)) | [].
-type nonempty_list(A) :: cons(A, list(A)).
-type two_or_more(A) :: cons(A, cons(A, list(A))).
-type maybe_improperly_nonempty...

We also get exact list and string types:

-type yes_or_no() :: cons($y, cons($e, cons($s, []))) |
                     cons($n, cons($o, [])).

Unions of strings can be represented as tries:

-type fry_or_frog() :: cons($f, cons($r, cons($y, []) |
                                         cons($o, cons($g, [])))).

We can also infer string literals as exact string types.

If we do this, it should probably be restricted by an option (e.g. exact_list_types).