Stop more cases of infinite recursion #361
Conversation
There was a problem hiding this comment.
This is great work! Thanks for fixing these loop bugs.
I do have a comment about simplifying the way termination works in normalize.
I'd be willing to accept this as is, even if it invalidates some tests, because is dinitively fixes the problem of looping. The tests that fail are related to refinement and, while we should eventually fix those as well, they don't rank as important to me as the looping bugs. Though there is a clear tradeoff here. @zuiderkwast WDYT?
| normalize({type, _, record, [{atom, _, Name}|Fields]}, TEnv) when length(Fields) > 0 -> | ||
| NormFields = [type_field_type(FieldName, normalize(Type, TEnv)) | ||
| || ?type_field_type(FieldName, Type) <- Fields], | ||
| -spec normalize(type(), tenv()) -> type(). |
There was a problem hiding this comment.
I think a simpler, a cheaper way to fix the problem in normalize would be to keep track of whether we are at the "top level" of a type, where we unfold user-defined types, or whether we are deeper down and don't normalize them. That way we wouldn't need to carry a map of unfoldings. The final result would be the same, I believe.
test/should_fail/infinite_loop4.erl
Outdated
| %% The following are two variants of the above: | ||
| %% - when the pattern matches the type used for A | ||
| %% - and when it doesn't | ||
| -spec unwrap1(rec1(integer())) -> ok. | ||
| unwrap1(_) -> ok. |
There was a problem hiding this comment.
Here, it's expected that ok :: A which passes because we don't solve the constraints on type variables. That's why it fail IIUC. I think we can live with that and move this to a type var constraint solver known problem.
There was a problem hiding this comment.
Btw, the names of the test cases "infinite_loop4" and similar are not that great, especially when the're not infinite loops anymore. :-) Better describe them as "recursive record with type variable" or similar.
Prior to this commit, the Env got passed around, but was not really used by normalize(). This meant that even an invalid Env didn't trigger any bugs. Now that we're using the Env to get the union size limit, it started triggering bugs where the env was not correctly adjusted to env() from tenv().
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 identified the problem with recursives types in josefs#322 and offered a nice example program to demonstrate the problem. Fixes josefs#322 although the program is still not accepted as it should be so I'm adding it to the known problems.
erszcz
force-pushed
the
stop-infinite-recursion-2
branch
from
4fade56
to
b59c8b3
Compare
|
Closing this one. Please see #368. |
This builds on top of #356 and #324 and breaks all cycles summed up in #324 (comment). It also terminates on the original example posted in #322. Together with the fixes from https://github.com/erszcz/Gradualizer/tree/start-app-in-rebar-plugin it also terminates on the example project from #360.
Apparently, this breaks a few existing tests, so I'm leaving it as a draft for now.