Fix some self-gradualization errors #408

erszcz · 2022-04-03T13:05:15Z

This builds on top of #404, which cleans up a considerable number of regressions from make gradualize output, and improves on it by fixing spec errors and other type issues in Gradualizer itself.

It's also a good exercise to find bugs in Gradualizer or spot hard to type check Erlang idioms.

Before this PR (but already with #404):

$ make gradualize | wc -l
make: *** [gradualize] Error 1
     619

With this PR:

$ make gradualize | wc -l
make: *** [gradualize] Error 1
     352

zuiderkwast · 2022-04-04T01:02:08Z

src/gradualizer_int.erl

+-type extended_int_type() :: {type, erl_anno:anno(), range, [{integer, erl_anno:anno(), int()}]}
+                           | {'integer', erl_anno:anno(), integer()}.
+%% `extended_int_type' is needed to describe type representations
+%% which are not part of `gradualizer_type:abstract_type()'.


Why is this not a subtype to type()?

In ranges, if we use pos_inf or neg_inf, it's not wrapped in a {integer, Anno, _} tuple, see

Gradualizer/src/gradualizer_type.erl

Lines 276 to 277 in 3cda2e5

-type af_range_integer_type() :: 'pos_inf' | 'neg_inf'

| af_singleton_integer_type().

With integers, the number is always a non_neg_integer(), if it has to be a negative value, it's wrapped in a unary minus op node, see

Gradualizer/src/gradualizer_type.erl

Line 298 in 3cda2e5

-type af_integer() :: {'integer', anno(), non_neg_integer()}.

zuiderkwast

Very nice!

src/gradualizer_type.erl

zuiderkwast · 2022-04-04T01:19:28Z

src/gradualizer_lib.erl

 get_type_definition({remote_type, _Anno, [{atom, _, Module}, {atom, _, Name}, Args]}, _Env, _Opts) ->
+    %% We matched out the non-type() elements above so we can assert Args :: [type()]
+    Args = ?assert_type(Args, [type()]),


Why? Atom literals are part of abstract_type().

Atom literals can be represented by type(), but literal atoms are not of type type(), see

Gradualizer/src/gradualizer_type.erl

Lines 290 to 292 in 3cda2e5

-type af_atom() :: af_lit_atom(atom()).

-type af_lit_atom(A) :: {'atom', anno(), A}.

abstract_type() includes af_atom().

Gradualizer/src/gradualizer_type.erl

Lines 202 to 203 in 3cda2e5

-type abstract_type() :: af_annotated_type()

| af_atom()

Doesn't this imply that {atom, anno(), atom()} :: abstract_type()?

Ahh, sorry, my above comment is nonsense, as the atoms here are actually in the AST representation. Let me check again...

Ok, so we start with this error:

$ gradualizer -I include/ -- src/gradualizer_lib.erl src/gradualizer_lib.erl: The variable on line 112 at column 43 is expected to have type [type()] but it has type [abstract_type()] | {atom, anno(), atom()} %% We matched out the non-type() elements above so we can assert Args :: [type()] %Args = ?assert_type(Args, [type()]), gradualizer_db:get_type(Module, Name, Args); ^^^^

We check the type of a remote call node:

Gradualizer/src/gradualizer_type.erl

Lines 254 to 257 in 3cda2e5

-type af_remote_type() ::

{'remote_type', anno(), [(Module :: af_atom()) |

(TypeName :: af_atom()) |

[abstract_type()]]}. % [Module, Name, [T]]

So Args is a [type()], not a type(), which is fine for passing down. Singleton atoms are not fine, as we need a list. We know we've already matched on the singleton atoms, so by elimination we're safe to assert Args :: [type()].

Great! Only the comment needs an update then. E.g. %% We matched out the single atom arguments, so only Args (list-of-type) remains.

src/typechecker.erl

zuiderkwast · 2022-04-04T01:30:27Z

src/typechecker.erl

-refine_ty(?type(list, E), ?type(nonempty_list, E), _, _Env) ->
-    type(nil);
+refine_ty(?type(list, [ElemTy1]), ?type(nonempty_list, [ElemTy2]), Trace, Env) ->
+    case refine(ElemTy1, ElemTy2, Trace, Env) of


🍰🎂🥧🍺

zuiderkwast · 2022-04-04T01:35:31Z

src/typechecker.erl

@@ -4227,14 +4250,15 @@ add_type_pat(CONS = {cons, P, PH, PT}, ListTy, Env, VEnv) ->
            TailTy = normalize(type(union, [ListTy, type(nil)]), Env),
            {_TailPatTy, _TauUBound, VEnv3, Cs} = add_type_pat(PT, TailTy, Env, VEnv2),
            NonEmptyTy = rewrite_list_to_nonempty_list(ListTy),
-            {NonEmptyTy, NonEmptyTy, VEnv3, Cs};
+            {type(none), NonEmptyTy, VEnv3, Cs};


[_|_] exhausts nonempty list. Have you saved that for another PR?

Hmmm, I have to think it through 🤔

I think it's only the pattern [A | B] where A and B are free variables (not in VEnv) that works.

zuiderkwast · 2022-04-04T09:38:42Z

src/typechecker.erl

            NonEmptyTy = rewrite_list_to_nonempty_list(ListTy),
-            {NonEmptyTy, NonEmptyTy, VEnv3, constraints:combine([Cs1, Cs2, Cs3])};
+            {PatTy, NonEmptyTy, VEnv3, constraints:combine([Cs1, Cs2, Cs3])};


Here, I think we should return {none(), ...} too, in the normal case.

Only if the pattern is match-all ([A|B] where A and B are free, or A is bound and ElemTy is a singleton type) the pattern exhausts the type. In that case, we can return PatTy I suppose.

See the comment above add_types_pats about the return tuple {PatTys, UBounds, NewVEnv, Constraints}:

%% The returned lists of types are interpreted like this: %% PatTy :: Pat as if Pat were a type. For match-all patterns, PatTy %% is the same as the type. For patterns matching a singleton type, PatTy %% is the singleton type. Otherwise, PatTy is none(). PatTy is a type exhausted %% by Pat. UBound is Ty or a subtype such that Pat :: UBound.

erszcz · 2022-04-05T16:02:09Z

@zuiderkwast I've given your points about exhaustive list types some thought. I also considered if just looking at whether the patterns match fixed length lists or any lists is sufficient - I'm afraid it's not :/ It seems that to model cases like these:

-spec i([atom()]) -> ok.
i([]) -> ok;
i([Cs]) -> ok;
i([C1, C2 | Cs]) -> ok.

-spec j([atom()]) -> ok.
j([]) -> ok;
j([C1, C2 | _]) -> ok;
j([Cs]) -> ok.

it's necessary to track the lengths of the patterns. Please see #405 (comment) for a bit more detail.

zuiderkwast · 2022-04-05T20:17:51Z

it's necessary to track the lengths of the patterns

For clauses that exhaust a list using patterns [], [X] and [X, Y | Z], we can't perform exhaustiveness-checking without encoding the list length in the type, but that doesn't mean we can't silence the false positives and make it pass.

I believe we can run into similar problems for other types and there will always be something we can't do, unless we continue to extend the type language over and over. I'm not saying we can't do that, but I'm almost certain that we'll run into a lot of times when we need to decide how subtyping, GLB, refinement, etc. work for these types. We need draw the line somewhere. (We already have some overly fancy logic for arithmetic operators, for example, that I think we could live without, to make the type system simpler, but I know others think it's worth it.)

zuiderkwast · 2022-04-05T20:25:11Z

Assume we add list(T, N) and list(T, N+) types.

Should we be able do exhaustiveness-checking for the following?

-spec q([fruit()]) -> fruit().
q([X | Xs]) when length(Xs) rem 2 == 0 ->
    X;
q(Xs) when length(Xs) rem 2 == 0 ->
    bananas.

(We could solve it if we encode odd and even lengths of lists in the type. Not saying we should.)

erszcz · 2022-05-30T08:23:12Z

The current status is:

10:02:04 erszcz @ x6 : ~/work/erszcz/gradualizer ((a72e7f0...) %)
$ make gradualize | wc -l
make: *** [gradualize] Error 1
     485

on master versus

10:02:24 erszcz @ x6 : ~/work/erszcz/gradualizer (fix-self-gradualization-errors %)
$ make gradualize | wc -l
make: *** [gradualize] Error 1
     361

on this branch. Less of a difference, but still worth it.

erszcz requested a review from zuiderkwast April 3, 2022 13:05

This was referenced Apr 3, 2022

Refactor throw_orig_type to avoid guards -> improve self-gradualization #407

Closed

int_range() is not a subtype of type() but it's used like it is #406

Open

zuiderkwast reviewed Apr 4, 2022

View reviewed changes

erszcz force-pushed the fix-self-gradualization-errors branch from 932f2f1 to a57bf6c Compare April 5, 2022 16:12

zuiderkwast mentioned this pull request Apr 5, 2022

"The clause ... cannot be reached" when matching on list patterns #405

Open

erszcz force-pushed the fix-self-gradualization-errors branch from a57bf6c to abec87f Compare April 7, 2022 22:03

erszcz added 6 commits May 30, 2022 09:49

Fix self-gradualize error in gradualizer.erl

67d6bf9

Fix self-gradualize errors in gradualizer_int.erl

a955657

Fix self-gradualize errors in gradualizer_lib.erl

a7ae329

Fix env() record definition access

e011920

Fix self-gradualize errors in typechecker.erl

3a4f77e

Unify speccing Env as env() instead of #env{}

1a30b38

erszcz force-pushed the fix-self-gradualization-errors branch from abec87f to 1a30b38 Compare May 30, 2022 08:01

erszcz merged commit 6ae3298 into josefs:master May 30, 2022

erszcz deleted the fix-self-gradualization-errors branch May 30, 2022 08:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix some self-gradualization errors #408

Fix some self-gradualization errors #408

erszcz commented Apr 3, 2022 •

edited

Loading

zuiderkwast Apr 4, 2022

erszcz Apr 4, 2022

zuiderkwast left a comment

zuiderkwast Apr 4, 2022

erszcz Apr 4, 2022

zuiderkwast Apr 4, 2022 •

edited

Loading

erszcz Apr 4, 2022 •

edited

Loading

erszcz Apr 4, 2022

zuiderkwast Apr 4, 2022

zuiderkwast Apr 4, 2022

zuiderkwast Apr 4, 2022

erszcz Apr 4, 2022

zuiderkwast Apr 4, 2022

zuiderkwast Apr 4, 2022

zuiderkwast Apr 4, 2022

erszcz commented Apr 5, 2022

zuiderkwast commented Apr 5, 2022

zuiderkwast commented Apr 5, 2022 •

edited

Loading

erszcz commented May 30, 2022

	-type af_range_integer_type() :: 'pos_inf' \| 'neg_inf'
	\| af_singleton_integer_type().

	-type af_atom() :: af_lit_atom(atom()).

	-type af_lit_atom(A) :: {'atom', anno(), A}.

	-type af_remote_type() ::
	{'remote_type', anno(), [(Module :: af_atom()) \|
	(TypeName :: af_atom()) \|
	[abstract_type()]]}. % [Module, Name, [T]]

Fix some self-gradualization errors #408

Fix some self-gradualization errors #408

Conversation

erszcz commented Apr 3, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zuiderkwast left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zuiderkwast Apr 4, 2022 • edited Loading

Choose a reason for hiding this comment

erszcz Apr 4, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erszcz commented Apr 5, 2022

zuiderkwast commented Apr 5, 2022

zuiderkwast commented Apr 5, 2022 • edited Loading

erszcz commented May 30, 2022

erszcz commented Apr 3, 2022 •

edited

Loading

zuiderkwast Apr 4, 2022 •

edited

Loading

erszcz Apr 4, 2022 •

edited

Loading

zuiderkwast commented Apr 5, 2022 •

edited

Loading