Normalize away annotated types

[gomoripeti]

This small change triggers a new "infinite loop" while self-gradualizing
possibly again in GLB. A somewhat minimal extract of
typechecker:type_check_comprehension_on which triggers the behaviour
is put into should_pass/glb_ann_types.erl.

Should not be merged! Needs to be investigated.

[zuiderkwast]

Nice!

Now that ann_type is not present in normalized types, perhaps some clauses for ann_type in functions expecting normalized types can be removed?

It would be nice of course to isolate the problem and make a stand-alone test case with the required type definitions defined within the module. If that's hard, then this is fine.

[zuiderkwast]

?TYPE_MOD here?

[zuiderkwast]

?TYPE_MOD here?

[gomoripeti]

indeed. (but this whole testcase is just temporary to help track down the issue)

[zuiderkwast]

gradualizer_tests: type_check_dir_test...*timed out*

Perhaps there is another infinite loop?

[zuiderkwast]

Btw, I think the title is slightly confusing. I'm not 100% sure about the terminology, but my intuition says that type annotations is stuff annotated with types, while annotated types is types annotated with stuff.

[gomoripeti]

I tried hard to get the title right but in that late hour I picked the wrong choice :)

[gomoripeti]

type_check_dir_test runs all the should_pass testcases, also the one that is a negative example. So (I really hope) there is just one infinite loop.

When I hit this issue I didnt want to go any further before it is addressed (removing ann_type's from everywhere else). This issue is most probably not related to ann_type but until now Gradualizer would error out before reaching the issue.

[josefs]

Sorry for being blunt, I think this is the wrong way forward. We should be checking the ann_types so that they make sense, otherwise it's going to be very confusing for programmers.

[Zalastax]

Some notes:

If T is a type definition Name :: Type, where Name is a variable and Type is a type, then Rep(T) = {ann_type,LINE,[Rep(Name),Rep(Type)]} (from absform).

----------------------------------------

Type variables can be used in specifications to specify relations for the input and output arguments of a function. For example, the following specification defines the type of a polymorphic identity function:

  -spec id(X) -> X.

Notice that the above specification does not restrict the input and output type in any way. These types can be constrained by guard-like subtype constraints and provide bounded quantification:

  -spec id(X) -> X when X :: tuple().

Currently, the :: constraint (read as «is a subtype of») is the only guard constraint that can be used in the when part of a -spec attribute.

Note

The above function specification uses multiple occurrences of the same type variable. That provides more type information than the following function specification, where the type variables are missing:

  -spec id(tuple()) -> tuple().

The latter specification says that the function takes some tuple and returns some tuple. The specification with the X type variable specifies that the function takes a tuple and returns the same tuple.

However, it is up to the tools that process the specifications to choose whether to take this extra information into account or not.
(from typespec).

----------------------------------------

Do we want to take that extra information into account? I suspect that no tool takes advantage of the extra information and that most specs that reuse the same variable does so accidentally. I would opt for ignoring it and lobby for OTP to replace that note to instead say that it doesn't have to return the same thing.

@josefs was this what you meant with checking so they make sense? What do we loose by normalizing?

[gomoripeti]

@Zalastax I think there are two things here: type variables in general and annotated types specifically.

Re: annotated types let's discuss in #180

[zuiderkwast]

Closing this in favor of #228, which is basically the same change.