Gradualizer Make sure not to recurse forever in typechecker:normalize()

Given a recursive type, typechecker:normalize() can recurse forever if we don't take care to stop the recursion. This patch adds a set to keep track of the types that normalize has unfolded so far and stops unfolding if asked to normalize a type that has already been unfolded.

@ilya-klyuchnikov identified the problem with recursives types in #322 and offered a nice example program to demonstrate the problem.

Fixes #322 although the program is still not accepted as it should be so I'm adding it to the known problems.

Mar 29 '21 14:03 josefs

Just FYI - #323 - a naive fix to not get into the loop. (I have not read this PR yet fully)

Mar 29 '21 14:03 ilya-klyuchnikov

Just thinking about @zuiderkwast's remarks, this example makes gradualizer fall into the loop.

-module(recursive_record).

-compile([export_all, nowarn_export_all]).

-type rec(A) :: A | #rec{rec :: A | rec(A)}.
-record(rec, {rec :: any()}).

-spec unwrap(rec(#rec{rec :: A})) -> rec(A).
unwrap(#rec{rec = Rec}) -> Rec.

./bin/gradualizer recursive_record.erl

Mar 29 '21 18:03 ilya-klyuchnikov

@ilya-klyuchnikov are you saying we also need the set mechanism for recursive records? [Edit] ... and refined record types

Mar 29 '21 18:03 zuiderkwast

are you saying we also need the set mechanism for recursive records?

Yes, - in this example with records - the loop happens at line 619. - Where a (parameterized) record is normalized.

Mar 29 '21 18:03 ilya-klyuchnikov

Perhaps just it needs some small tweak to solve the known problem..?

Yes, I think there should be a way to fix what I have to make the counter example of @ilya-klyuchnikov typecheck. Not sure exactly what that tweak is though.

Mar 29 '21 21:03 josefs

@ilya-klyuchnikov I'm too stupid to figure out why your recursive record example loops. To me it seems like if it's going to loop forever it needs to unfold the recursive type forever, and that should be taken care of by the mechanism that I've implemented in this PR. However, that's clearly not the case. But I need help figuring out where exactly the problem is.

Mar 30 '21 10:03 josefs

It seems, that records in the first place may not be the most essential part of reproducing/minimizing the issue.

Just trying identifying the loop manually - dumping stack trace, it seems that the loop is flatten_unions -> normalize_rec -> flatten_unions

Stack
[{typechecker,flatten_unions,3,[{file,"src/typechecker.erl"},{line,766}]},
 {typechecker,normalize_rec,3,[{file,"src/typechecker.erl"},{line,624}]},
 {typechecker,'-normalize_rec/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,620}]},
 {typechecker,normalize_rec,3,[{file,"src/typechecker.erl"},{line,621}]},
 {typechecker,'-flatten_unions/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^1/1-1-',4,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^1/1-1-',4,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,normalize_rec,3,[{file,"src/typechecker.erl"},{line,624}]},
 {typechecker,'-normalize_rec/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,620}]},
 {typechecker,normalize_rec,3,[{file,"src/typechecker.erl"},{line,621}]},
 {typechecker,'-flatten_unions/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^1/1-1-',4,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^1/1-1-',4,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,normalize_rec,3,[{file,"src/typechecker.erl"},{line,624}]},
 {typechecker,'-normalize_rec/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,620}]},
 {typechecker,normalize_rec,3,[{file,"src/typechecker.erl"},{line,621}]},
 {typechecker,'-flatten_unions/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^1/1-1-',4,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,'-flatten_unions/3-lc$^1/1-1-',4,
              [{file,"src/typechecker.erl"},{line,769}]},
 {typechecker,normalize_rec,3,[{file,"src/typechecker.erl"},{line,624}]},
 {typechecker,'-normalize_rec/3-lc$^0/1-0-',3,
              [{file,"src/typechecker.erl"},{line,620}]},
...

However, - it's possible to loop without records!

-module(more_recursive_types).

-compile([export_all, nowarn_export_all]).

-type rec1(A) :: A | rec1({A | rec1(A)}).

-spec unwrap(rec1(A)) -> atom().
unwrap({rec, Z}) -> Z.

In this case the loop happens in refine:

Stack
[{typechecker,flatten_unions,3,[{file,"src/typechecker.erl"},{line,766}]},
 {typechecker,normalize_rec,3,[{file,"src/typechecker.erl"},{line,624}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3340}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},
 {lists,foldr,3,[{file,"lists.erl"},{line,1280}]},
 {typechecker,refine_ty,3,[{file,"src/typechecker.erl"},{line,3376}]},
 {typechecker,refine,3,[{file,"src/typechecker.erl"},{line,3341}]},
 {typechecker,'-refine_ty/3-fun-6-',4,
              [{file,"src/typechecker.erl"},{line,3377}]},

My intuition says that usage of unions may be essential in both cases.

Mar 30 '21 16:03 ilya-klyuchnikov

It's also possible to loop without type parameters:

-module(even_more_recursive_types).

-compile([export_all, nowarn_export_all]).

-type rec1() :: rec1 | {rec1, rec1()} | {rec1, {rec1, rec1()}}.

-spec unwrap(rec1()) -> rec1().
unwrap({_, Z}) -> Z.

Mar 30 '21 19:03 ilya-klyuchnikov

Having tracked down one of the infinite loops to a problem in glb - https://github.com/josefs/Gradualizer/pull/356 - I tried this PR rebased on top of the glb one - https://github.com/erszcz/Gradualizer/tree/wip-recursive-types. I also made sure the set carried through normalize_rec stores type arity in case of user types. Alas, I think there's more than one problem here. I added all the code snippets from this PR to the repo (sorry for the mess, but it's just a quick hack now).

Here's a summary of the tests:

norm_test.erl is the one from the glb PR - this works fine
norm_test2.erl is @josefs's -type apa(A) :: A | apa({A}). - this also works fine
loop_test3.erl is @ilya-klyuchnikov's recursive records example - this seems to loop somewhere in typechecker:flatten_unions
loop_test4.erl is @ilya-klyuchnikov's looping without records - this loops in typelib:remove_pos
loop_test5.erl is @ilya-klyuchnikov's even_more_recursive_types - this seems to be a bigger cycle with normalize and glb

I think the test cases listed in this thread uncover more than one place where we hit an infinite loop. It also seems to me that the sets:is_element check in just one of normalize_rec clauses is not enough - I think we have to make that check in each clause which calls normalize_rec recursively - similarly to how refinable does it with stop_refinable_recursion.

All in all, there's more work to be done here, but there's some light at the end of the tunnel. The dbg invocation I use is available on the wip-recursive-types I link to in the first paragraph.

Oct 15 '21 07:10 erszcz

@erszcz Do you have a plan here? If you have updates to this PR, just open a new PR and then we'll close this one.

Oct 20 '21 10:10 zuiderkwast

I don't have more updates than my former comment here, but I'd like to take a closer look at this when time permits. So far it seems that the loop in normalize is crucial, but that there might be more looping functions throughout the code. I'll post fixes as I come up with any :+1:

Oct 20 '21 10:10 erszcz

I'm closing this because of #458 already being merged.

Sep 26 '22 09:09 erszcz

Gradualizer Gradualizer copied to clipboard

Make sure not to recurse forever in typechecker:normalize()

Gradualizer
Gradualizer copied to clipboard